Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$ I'm struggling to proof this both if I use or introduction rule $\lor_{I_1}$ (to work on $D$) or or introduction rule $\lor_{I_2}$ (to work on $C \lor E$). Could you help me? 
 A: 
Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

Here is a skeleton; just flesh it out.   The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.
$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{(A \to \lnot B \lor C)\\ ((\lnot D \land A) \to B)\\ (\lnot E \to A) }{\fitch{\lnot(D\lor (C\lor E))}{\fitch{~}{~\\~\\\fitch{~}{\fitch{~}{~\\~\\\bot}\\~\\~\\D\lor(B\lor E)\\\bot}\\~\\\fitch{~}{~\\D\lor(C\lor E)\\\bot}\\~\\\bot}\\~\\~\\~\\D\lor(C\lor E)\\\bot}\\~\\D\lor (C\lor E)}$$
A: $A \implies \lnot B \lor C$ is equivalent to $\lnot B\lor C$ or $\lnot A$
$\lnot D \land A \implies B $ is equivalent to $B$ or $D\lor \lnot A$
$\lnot E \implies A$ is equivalent to $A$ or $E$
So you want to prove that $\lnot A \lor \lnot B\lor C$, $\lnot A\lor B\lor D$, $A\lor E$ gives you $C\lor D\lor E$. Can you show this last step?
A: We will work by contradicition, starting assuming :
1) $\lnot [D \lor (C \lor E)]$ --- assumed [a]
2) $\lnot D$ --- assumed [b]
3) $\lnot E$ --- assumed [c]
4) $A$ --- from 3) and premise-3
5) $\lnot D \land A$ --- from 2) and 4)
6) $B$ --- from 5) and premise-2
7) $\lnot B \lor C$ --- from 4) and premise-1
Now we need $\lor$-elim on 7)
8) $\lnot B$ --- assumed [d1] from 7)
9) $\bot$ --- contradiction ! with 6) and 8)
10) $C$ --- assumed [d2] from 7)
11) $C \lor E$ --- from 10)
12) $D \lor (C \lor E)$ --- from 11)
13) $\bot$ --- contradiction ! with 1) and 12)
We have derived $\bot$ in both cases of the $\lor$-elim; thus we have :

14) $\bot$ --- from 8)-9) and 10)-13) and 7) by $\lor$-elim, discharging assumptions [d1] and [d2]

15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]
16) $C \lor E$ --- from 15)
17) $D \lor (C \lor E)$ --- from 16)
18) $\bot$ --- contradiction ! with 1) and 17)
19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]
20) $D \lor (C \lor E)$ --- from 19)
21) $\bot$ --- contradiction ! with 1) and 20)


22) $D \lor (C \lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].


A: Here is a proof using the Law of Excluded Middle (LEM). Links to the text explaining the terms and the proof checker are at the bottom.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
