= Solution
Use the <disjunction elimination rule> on the outer disjunction. In its left branch, assume $P\lor Q$ and apply the <disjunction elimination rule> again: from a case assumption $P$, the <disjunction introduction rule> gives $P\lor R$; from a case assumption $Q$, the premise $Q\to R$ and the <modus ponens rule> give $R$, then the <disjunction introduction rule> gives $P\lor R$. Discharging those two inner case assumptions yields $P\lor R$ under the left outer branch.
In the right outer branch, assume $R\lor S$. A case assumption $R$ gives $P\lor R$ by the <disjunction introduction rule>. A case assumption $S$, together with the premise $\neg S$, gives $\bot$ by the <negation elimination rule>, and then $P\lor R$ by <logical falsity elimination rule>. Discharge these inner case assumptions with the <disjunction elimination rule>.
Both outer branches now have the same conclusion. Discharge the two outer case assumptions with the <disjunction elimination rule> to obtain \b[$P\lor R$] under exactly the stated premises.
Back to article page
