Natural Deduction Proof: (A ∨ B) ∧ (A ∨ C) ∴ A ∨ (B ∧ C)

Question

I've been having trouble figuring out how to prove the above statement. Frankly I'm only certain in my work insofar as splitting up the premise statement into (A v B) and (A v C). I've tried using rule of explosion to prove A or B but I just can't see how I can get the statement A or (B^C) out of the sub proof. Below is a snippet of my work, any and all help would be appreciated. (Pardon the odd formatting I tried my best to make my work as legible as possible)

1 (A ∨ B) ∧ (A ∨ C)
2 A ∨ B ∧E 1
3 A ∨ C ∧E 1
4 ¬A
5 A
6 ⊥ ¬E 4, 5

7 C X 6

8 C
9 C ∨E 3, 5–7, 8–8

Answer 1

Restarting from line 4. To use $A\lor B$ (2), first prove the two cases $A\to A\lor(B\land C)$ and $B\to A\lor(B\land C)$.

The latter means a subproof assuming $B$. In this subproof, to use $A\lor C$ (3), again prove the two cases $A\to A\lor (B\land C)$ (a repeat) and $C\to A\lor(B\land C)$. Therefore $A\lor (B\land C)$ by disjunction elimination (assuming $B$).

From $A\to A\lor (B\land C)$, $B\to A\lor (B\land C)$, $A\lor B$, therefore $A\lor (B\land C)$ by disjunction elimination.

Answer 2

That's (more or less) Exercise 21 (a) 4 in my Introduction to Formal Logic (CUP 2020 edition).

Of course, you aren't supposed to know that! :-)

But if you are having trouble with this sort of natural deduction proof, you might well find the book (or at least the ND chapters) helpful.

It is now freely available for download from https//www.logicmatters.net/ifl where you will also find links to very extensive worked answers to lots of exercises.

In particular, in the worked answers, I talk through the answer to your problem building up the proof in stages, starting at the bottom of p. 4, in this answer set.