Theorem exptOLD

Obsolete version of expt as of 25-May-2026. Exportation theorem pm3.3 (closed form of ex) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion

\( \vdash (\neg (\varphi \rightarrow \neg \psi) \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi \)

Proof

pm3.2im

imim1d _

com12 _