Theorem ecase3

Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)

Hypotheses
ecase3.1
\( \vdash \varphi \rightarrow \chi \)
ecase3.2
\( \vdash \psi \rightarrow \chi \)
ecase3.3
\( \vdash \neg (\varphi \vee \psi) \rightarrow \chi \)
Conclusion
\( \vdash \chi \)
Proof
l0
ecase3.1
ecase3.2
l2
jaoi l0 _
\( \vdash \varphi \vee \psi \rightarrow \chi \)
ecase3.3
\( \vdash \neg (\varphi \vee \psi) \rightarrow \chi \)
pm2.61i l2 _