# Formal proof of distributivity of conjuction

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?

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:

1. $$q$$ (assumption, from 3)

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

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

Case 2:

1. $$r$$ (assumption, from 3)

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

3. $$(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).

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)$$