Theorem pm2.61ii

Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses
pm2.61ii.1
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \chi \)
pm2.61ii.2
\( \vdash \varphi \rightarrow \chi \)
pm2.61ii.3
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \chi \)
Proof
l0
pm2.61ii.2
\( \vdash \varphi \rightarrow \chi \)
l1
pm2.61ii.1
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \chi \)
pm2.61ii.3
\( \vdash \psi \rightarrow \chi \)
pm2.61d2 l1 _
\( \vdash \neg \varphi \rightarrow \chi \)
pm2.61i l0 _