Theorem impexp

Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
pm3.3
pm3.31
impbii l0 _