Theorem expt

Exportation theorem pm3.3 (closed form of ex) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Garrett Katz, 25-May-2026.)

Conclusion
\( \vdash (\neg (\varphi \rightarrow \neg \psi) \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
pm3.2im
\( \vdash \varphi \rightarrow \psi \rightarrow \neg (\varphi \rightarrow \neg \psi) \)
id
\( \vdash (\neg (\varphi \rightarrow \neg \psi) \rightarrow \chi) \rightarrow \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
syl9r l0 _