Theorem 3ecase

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

Hypotheses
3ecase.1
\( \vdash \neg \varphi \rightarrow \theta \)
3ecase.2
\( \vdash \neg \psi \rightarrow \theta \)
3ecase.3
\( \vdash \neg \chi \rightarrow \theta \)
3ecase.4
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \theta \)
Proof
3ecase.4
l1
3exp _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
3ecase.1
2a1d _
\( \vdash \neg \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
l4
pm2.61i l1 _
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
l5
3ecase.2
\( \vdash \neg \psi \rightarrow \theta \)
3ecase.3
\( \vdash \neg \chi \rightarrow \theta \)
pm2.61nii l4 l5 _