Theorem expi

An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)

Hypothesis
expi.1
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
pm3.2im
\( \vdash \varphi \rightarrow \psi \rightarrow \neg (\varphi \rightarrow \neg \psi) \)
expi.1
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
syl6 l0 _