Theorem ecase

Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)

Hypotheses
ecase.1
\( \vdash \neg \varphi \rightarrow \chi \)
ecase.2
\( \vdash \neg \psi \rightarrow \chi \)
ecase.3
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \chi \)
Proof
ecase.3
l1
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l2
ecase.1
\( \vdash \neg \varphi \rightarrow \chi \)
ecase.2
\( \vdash \neg \psi \rightarrow \chi \)
pm2.61nii l1 l2 _