Natural deduction proof for new var 
Show by natural deduction,
$$(x \vee y) \vdash ((x \wedge z) \vee (z \implies y))$$

I have tried using $$(z \implies y)$$ as my assumption, but that didn't work out too well.
Where can I go?
 A: Here's one way of proving it using purely the rules of natural deduction:
\begin{array}{l}
& \{1\} & 1. & x \lor y & \text{ $Prem.$ }\\
& \{2\} & 2. & x & \text{ Assum. (1st Disj.) }\\
& \{3\} & 3. & z & \text{ Assum. }\\
& \{2,3\} & 4. & x \land z & \text{ 2,3 $\land$I }\\
& \{2,3\} & 5. & (x \land z) \lor (z \implies y) & \text{ 4 $\lor$I }\\
& \{2\} & 6. & z \implies ((x \land z) \lor (z \implies y)) & \text{ 3,5 CP }\\
& \{7\} & 7. & \neg z & \text{ Assum. }\\
& \{8\} & 8. & \neg y & \text{ Assum. }\\
& \{3,8\} & 9. & \neg y \land z & \text{ 3,8 $\land$I }\\
& \{3,8\} & 10. & z & \text{ 9 $\land$E }\\
& \{3\} & 11. & \neg y \implies z & \text{ 8,10 CP }\\
& \{3,7\} & 12. & \neg \neg y & \text{ 7,11 MT }\\
& \{3,7\} & 13. & y & \text{ 12 DNE }\\
& \{7\} & 14. & z \implies y & \text{ 3,13 CP }\\
& \{7\} & 15. & (x \land z) \lor (z \implies y) & \text{ 14 $\lor$I }\\
& - & 16. & \neg z \implies ((x \land z) \lor (z \implies y)) & \text{ 7,15 CP }\\
& \{17\} & 17. & \neg ((x \land z) \lor (z \implies y)) & \text{ Assum. }\\
& \{17\} & 18. & z & \text{ 16,17 MT, DNE }\\
& \{2,17\} & 19. & \neg z & \text{ 6,17 MT }\\
& \{2,17\} & 20. & z \land \neg z & \text{ 18,19 $\land$I }\\
& \{2\} & 21. & (x \land z) \lor (z \implies y) & \text{ 17,20 RAA (1st Concl.)}\\
& \{22\} & 22. & y & \text{ Assum. (2nd Disj.) }\\
& \{3,22\} & 23. & y \land z & \text{ 3,22 $\land$I }\\
& \{3,22\} & 24. & y & \text{ 23 $\land$E }\\
& \{22\} & 25. & z \implies y & \text{ 3,24 CP }\\
& \{22\} & 26. & (x \land z) \lor (z \implies y) & \text{ 26 $\lor$I (2nd Concl.)}\\
& \{1\} & 27. & (x \land z) \lor (z \implies y)& \text{ 1,2,21,22,26 $\lor$E }\\
\end{array}
A: In the formula that has to be derived we have a logical disjunction as a major logical connective and we know that $p\to q \leftrightarrow \neg p\lor q$. Keeping these two things in mind helps us picking the appropriate assumption $z\land\neg y$.
$$
\begin{array}{l}
& \{1\} & (1) & x\lor y & \text {Premise}\\
& \{2\} & (2) & z \land\neg y & \text {Assumption}\\
& \{2\} & (3) & \neg y & \text {2 Simplification}\\
& \{1,2\} & (4) & x & \text {1,3 Modus tollendo ponens}\\
& \{2\} & (5) & z & \text {2 Simplification}\\
& \{1,2\} & (6) & x\land z & \text {4,5 Adjunction}\\
& \{1\} & (7) & (z\land\neg y)\to(x\land z) & \text {2,6 Conditional Proof}\\
& \{1\} & (8) & \neg(z\land\neg y)\lor(x\land z) & \text {7 Equivalence for Implication and Disjunction}\\
& \{1\} & (9) & (\neg z\lor y)\lor(x\land z) & \text {8 De Morgan's Law}\\
& \{1\} & (10) & (x\land z)\lor(z\to y) & \text {9 Equivalence for Implication and Disjunction and Commutative Law}\\
\end{array}$$
A: Hint: First 4 lines of a proof using a simplified form of natural deduction:


*

*$X\lor Y\space$  (Premise, two cases to consider)

*$Z\lor \neg Z\space$  (Law of excluded middle, two sub-cases to consider)

*$X\space$  (Premise, case 1)

*$Z\space$  (Premise, sub-case 1)
In every case and sub-case, you should be able to obtain $[X\land Y] \lor [Z\implies Y].$
A: Here is a proof using natural deduction with a Fitch-style proof checker.

The overall strategy was to use the law of the excluded middle (LEM) on $Z \lor \lnot Z$.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
A: $\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}$
Here's a proof by contradiction.
$${\fitch{~~1.~x\vee y\qquad\textsf{Premise}}{\fitch{~~2.~\neg((x\wedge z)\vee(z\to y))\qquad\textsf{Assumption}}{\fitch{~~3.~z\qquad\textsf{Assumption}}{\fitch{~~4.~x\qquad\textsf{Assumption}}{~~5.~x\wedge z\qquad\textsf{Conjunction Introduction (3,4)}\\~~6.~(x\wedge z)\vee(z\to y)\qquad\textsf{Disjunction Introduction (5)}\\~~7.~\bot\qquad\textsf{Negation Elimination (2,6)}\\~~8.~y\qquad\textsf{Ex Falso Quodlibet (7)}}\\~~9.~x\to y\qquad\textsf{Conditional Introduction (4-8)}\\\fitch{10.~y\qquad\textsf{Assumption}}{}\\11.~y\to y\qquad\textsf{Conditional Introduction (10-10)}\\12.~y\qquad\textsf{Disjunction Elimination (1,9,11)}}\\13.~z\to y\qquad\textsf{Conditional Introduction (3-12)}\\14.~(x\wedge z)\vee(z\to y)\qquad\textsf{Disjunction Introduction (13)}\\15.~\bot\qquad\textsf{Negation Elimination (2,14)}}\\16.~\neg\neg((x\wedge z)\vee(z\to y))\qquad\textsf{Negation Introduction (2-15)}\\17.~(x\wedge z)\vee(z\to y)\qquad\textsf{Double Negation Elimination (16)}}\\\therefore \quad x\vee y\vdash (x\wedge z)\vee(z\to y)}$$
