Conditional proof/contradiction, long example problem Here are the premises/conclusion, and where I've gotten so far. 
$1.$ $(W\wedge E)\rightarrow (P\vee L)$ (PR)
$2.$ $(W\wedge \neg E)\wedge R))\rightarrow (P\vee D)$ (PR)
$3.$ $((W\wedge \neg E)\wedge \neg R))\rightarrow (U\wedge \neg F)$ (PR)
$-.$ $(W\wedge F)\rightarrow (L\vee D)\vee P$ (CO)
$4.$ $\neg(U\wedge \neg F)\rightarrow \neg(W\wedge(\neg E\wedge \neg R))$ From $3$ transposition
$5.$ $(\neg U\vee \neg \neg F)\rightarrow \neg(W\wedge(\neg E\wedge \neg R))$ From $4$ DeM
$6.$ $(\neg U\vee F)\rightarrow \neg(W\wedge(\neg E\wedge \neg R))$ From $5$ Double negation
$7.$ $(\neg U\vee F) \rightarrow (\neg W\vee \neg (\neg E\wedge \neg R))$ From $6$ DeM
$8.$ $(\neg U \vee F)\rightarrow(\neg W\vee(\neg \neg E\vee \neg \neg R))$ From $7$ DeM
$9.$ $(\neg U \vee F)\rightarrow (\neg W \vee (E\vee R))$ From $8$ double negation
Here is where my conditional proof starts.
$10.$ $W\wedge F$ (Provisional assumption)
$11.$ $W$ From $10$ conjunction elimination (CE)
$12.$ $F$ From $10$ CE
$13.$ $\neg U \vee F$ From $12$ disjunctive addition (DA)
$14.$ $(\neg W\vee (E\vee R))$ From $9$, $13$ Modus Ponens
$15.$ $E\vee R$ From $14$, $11$ Disjunctive syllogism
At this point I'm lost. I've tried assuming several negations for reductio (contradiction) but I haven't gotten the desired result. Any ideas?
 A: Up to step 15 it's Ok.
We can use the Law of Excluded Middle : $E \lor \lnot E$ and proceed by cases (Disjunction Elimination).

(i)
Assuming $E$, we have $W \land E$ by Conjunction Introduction with step 11.
Thus, from premise (1) we conclude with $(P \lor L)$ by Modus Ponens and then with $(P \lor (L \lor D))$ by Disjunction Introduction (re-arranging the terms).
(ii)
Assuming $\lnot E$, we have $R$ from step 15 : $E \lor R$, by Disjunctive Syllogism. Thus we have $((W \land \lnot E) \land R)$ and we conclude from premise (2) by MP with : $(P \lor D)$, and again with $(P \lor (L \lor D))$ by Disjunction Introduction (re-arranging the terms).
Thus, from the assumption $(W \land F)$, we have proved $(P \lor (L \lor D))$ twice, both under assumption $E$ and under assumption $\lnot E$.
I.e., we have, by Conditional Proof :

$(W \land F) \vdash E \rightarrow (P \lor (L \lor D))$

and 

$(W \land F) \vdash \lnot E \rightarrow (P \lor (L \lor D))$.

With the Law of Excluded Middle, by Disjunction elimination, we can conclude with :

$(W \land F) \vdash (P \lor (L \lor D))$.

and by Conditional Proof with :


$(W \land F) \rightarrow (P \lor (L \lor D))$.



Added
If we nedd a proof of the tautology $E \lor \lnot E$, we can insert this "sub-proof" :
$W$ --- step 11 of the main proof
$E$ --- assumed for CP
$E \lor E$ --- by Disjunction introduction
$E$ --- by Tautology
$E \rightarrow E$ --- by CP

$\lnot E \lor E$ --- by Material implication.

A: The following proof using a Fitch-style proof checker attempts the problem directly by assuming the antecedent of the goal and deriving the consequent.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
