Theorem ecase3d

Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses
ecase3d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
ecase3d.2
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
ecase3d.3
\( \vdash \varphi \rightarrow \neg (\psi \vee \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
ecase3d.1
ecase3d.2
l2
jaod l0 _
\( \vdash \varphi \rightarrow \psi \vee \chi \rightarrow \theta \)
ecase3d.3
\( \vdash \varphi \rightarrow \neg (\psi \vee \chi) \rightarrow \theta \)
pm2.61d l2 _