Questionnaire-2024/natural_deduction_propositional_logic/0071_sol.tex

This sequent is provable.

\begin{logicproof}{1}
  (p \imp q) \land  (q \imp r) & \prem\\
  \neg r \lor q & \prem\\
  p \imp q & $\ande 1$ \\
  q \imp r & $\ande 1$ \\
  \begin{subproof}
    \neg r & \assum\\
    \neg q & $\MT 4, 5$ \\
    \neg p & $\MT 3, 6$ \\
    \neg p \lor r & $\ori 7$
  \end{subproof}
  \begin{subproof}
    q & \assum \\
    r & $\impe 9, 4$ \\
    \neg p \lor r & $\ori 10$
  \end{subproof}
  \neg p \lor r & $\ore 2, 5-8, 9-10$
\end{logicproof}