Proof of distributivity of $\land$ over $\lor$ using disjE in natural deduction I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf
I'm trying to understand its proof of
$$
P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R)
$$
which is given as
$$
\frac{
    \displaystyle
    \frac{
      P \land (Q \lor R)
    }{
      Q \lor R
     }
    \quad
    \frac{
      \displaystyle
      \frac{
        \displaystyle
        \frac{P \land (Q \lor R)}{P}
        \quad[Q]
      }{
        (P \land Q)
      }
    }{
      (P \land Q) \lor (P \wedge R)
    }
    \quad
    \frac{
      \displaystyle
      \frac{
        \displaystyle
        \frac{P \land (Q \lor R)}{P}
        \quad[R]
      }{
        (P \land R)
      }
    }{
      (P \land Q) \lor (P \wedge R)
    }
}
{
  (P \land Q) \lor (P \land R)
}
$$
I think I understand the application of the various rules: conjI, conjunct1, conjunct2, disjI1, disjI2. But I'm having trouble reasoning about how disjE is applied on the bottom step. The structure of the proof doesn't seem to match how the rule is given:
$$
\frac{P \lor Q\quad \begin{matrix}[P] \\ \vdots \\ R\end{matrix} \quad \begin{matrix}[Q] \\ \vdots \\ R\end{matrix}}{R}
$$
Specifically, for each of the $[P]$ and $[Q]$ terms in the rule (so $[Q]$ and $[R]$ in the proof) there is an extra premise(?) next to it, so it's not clear to me that disjE can be applied.
How disjE is applied here?
 A: The last rule in the given derivation in the OP does match with the general scheme of the rule for elimination of disjunction $\lor_E$ below (I only changed the letters with respect to the rule in the OP)
\begin{equation}\tag{1}
\frac{Q \lor R \quad \begin{matrix}[Q] \\ \vdots \\ P\end{matrix} \quad \begin{matrix}[R] \\ \vdots \\ P\end{matrix}}{P}\lor_E
\end{equation}
Indeed, in $(1)$, writing
$$\tag{2}
\begin{matrix}[Q] \\ \vdots \\ P\end{matrix}
$$
means that there is a derivation whose conclusion is $P$ and that a number (possibly 0) of occurrences of $Q$ among the assumptions for that derivation will be discharged by the rule $\lor_E$ in $(1)$. It does not exclude the possibility that in $(2)$ there are other assumptions (or other occurrences of the same assumption $Q$ that won't be discharged later by $\lor_E$). Said differently, $(2)$ does not mean that $Q$ is the only "legitimate" assumption that can be used to derive $P$.
In the given derivation in the OP, the subderivation below
$$\tag{3}
\displaystyle
    \frac{
      \displaystyle
      \frac{
        \displaystyle
        \frac{P \land (Q \lor R)}{P}
        \quad[Q]
      }{
        (P \land Q)
      }
    }{
      (P \land Q) \lor (P \wedge R)
    }
$$
perfectly matches the pattern in $(2)$. Indeed, $(3)$ is a derivation where there are two assumptions:

*

*$Q$, which will be discharged later by the rule $\lor_E$,

*$P \land (Q \lor R)$, which is a "legitimate" hypothesis according to the text of the exercise.

