Theorem ecased

Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)

Hypotheses
ecased.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \theta \)
ecased.2
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \theta \)
ecased.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
ecased.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \theta \)
l1
ecased.2
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \theta \)
l2
pm3.11
\( \vdash \neg (\neg \psi \vee \neg \chi) \rightarrow \psi \wedge \chi \)
ecased.3
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
syl5 l2 _
\( \vdash \varphi \rightarrow \neg (\neg \psi \vee \neg \chi) \rightarrow \theta \)
ecase3d l0 l1 _