Questionnaire-2024/natural_deduction_propositional_logic/0067_sol.tex

This sequent is provable.

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