Theorem pm2.61d1

Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)

Hypotheses
pm2.61d1.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
pm2.61d1.2
\( \vdash \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
pm2.61d1.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
pm2.61d1.2
a1i _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
pm2.61d l0 _