Theorem impi

An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)

Hypothesis
impi.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
Proof
impi.1
con3rr3 _
con1i _