Formal proof of distributivity of conjuction

Question

I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction.

0.                       (no premises)
   1.p and (q or r)      (assumption)
   2.p                   (and elimination from 1)
   3.q or r              (and elimination from 1)
Case 1:
     4. q                (assumption) 
     5. q and p          (and introduction)
Case 2:
     6. r
     7. ???
. 
.
.
.
(p and q) or (p and r)

I tried to obtain $p\land q$ in the subproof and then use $\lor$-introduction to get $(p\land q)\lor (p\land r)$. I considered cases, but in the case $r$ I don't see any way to get $p\land q$. Probably this is the wrong strategy?

Answer 1

The key point is that the last rule should be a $\lor$-elimination, not a $\lor$-introduction.

1. $p \land (q \lor r)$ (assumption)

2. $p$ ($\land_{elim_1}$, from 1)

3. $q \lor r$ ($\land_{elim_2}$, from 1)

   Case 1:

   4. $q$ (assumption, from 3)

   5. $p \land q$ ($\land_{intro}$, from 2 and 4)

   6. $(p \land q) \lor (p \land r)$ ($\lor_{intro_1}$, from 5)

   Case 2:

   7. $r$ (assumption, from 3)

   8. $p \land r$ ($\land_{intro}$, from 2 and 7)

   9. $(p \land q) \lor (p \land r)$ ($\lor_{intro_2}$, from 8)

4. $(p \land q) \lor (p \land r)$ ($\lor_{elim}$, from 3, 6 and 9).

Answer 2

In the case of $r$, infer $p \land r$, and use $\lor \ Intro$ to derive $(p \land q) \lor (p \land r)$ from that. Make sure to derive that statement in the first suproof with $q$ as well, and so with $\lor \ Elim$ you can then pull out $(p \land q) \lor (p \land r)$