Theorem pm2.61nii

Inference eliminating two antecedents. (Contributed by NM, 13-Jul-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

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