LPL Fitch Exercise 6.20 Help

Question

I have the premises

$A\lor B$, $A\lor C$

And the conclusion

$A\lor(B\land C)$

I am told that I will need to use a subproof within a subproof. I have been trying to do this for ages and I just don't know how to do this formally. I know that

$(A\lor B)\land(A\lor C)\Leftrightarrow A\lor(B\land C)$

Answer 1

1) $A \lor B$ --- 1st premise

2) $A \lor C$ --- 2nd premise

Start first sub-proof using $\lor$-elim on 1st premise :

4) $A$ --- assumed [a1] from $\lor$-elim from 1)

5) $A \lor (B \land C)$ --- from 4) by $\lor$-intro

6) $B$ --- assumed [a2] from $\lor$-elim from 1)

Start second sub-proof using $\lor$-elim on 2nd premise :

7) $A$ --- assumed [b1] from $\lor$-elim from 2)

8) $A \lor (B \land C)$ --- from 7) by $\lor$-intro

9) $C$ --- assumed [b2] from $\lor$-elim from 2)

10) $B \land C$ --- from 6) and 9) by $\land$-intro

11) $A \lor (B \land C)$ --- from 10) by $\lor$-intro

Now we can close the second sub-proof (the "inner" one) because we have derived $A \lor (B \land C)$ under both "branches" ([b1] and [b2]) of the 2nd $\lor$-elim and we can discharge the relevant assumptions : [b1] and [b2].

12) $A \lor (B \land C)$ --- from 2) and 7) and 9) by $\lor$-elim.

Having closed the second sub-proof, we have derived $A \lor (B \land C)$ under both branches ([a1] and [a2]) of the 1st $\lor$-elim.

Thus, we can close also the first sub-proof (the "outer" one), discharging the relevant assumptions : [a1] and [a2].

Thus we may conclude with :

13) $A \lor (B \land C)$ --- from 1) with 4) and 6) by $\lor$-elim.