Theorem impt

Importation theorem pm3.1 (closed form of imp) expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)

Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \neg (\varphi \rightarrow \neg \psi) \rightarrow \chi \)
Proof
l0
simprim
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \psi \)
simplim
imim1i _
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \neg (\varphi \rightarrow \neg \psi) \rightarrow \psi \rightarrow \chi \)
mpdi l0 _