Solution (source code)

= Solution

Keep the four given premises in context and assume $P$ under label $a$. The <modus ponens rule> applied to the first two premises gives $Q\lor R$ and $\neg S$. Apply the <disjunction elimination rule> to $Q\lor R$ as follows.

Under a case assumption $Q$, the premise $Q\to S$ gives $S$ by the <modus ponens rule>. Together with $\neg S$, the <negation elimination rule> gives $\bot$, and the supplied <logical falsity elimination rule> gives $R$. Under the other case assumption $R$, the required conclusion $R$ is already available. Discharge both case assumptions with the <disjunction elimination rule> to conclude $R$.

Finally discharge $a$ with the <implication introduction rule>, giving \b[$P\to R$]. The premise $S\to Q$ is not needed: a derivation is permitted to leave a premise unused.