Theorem con34b

A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg \psi \rightarrow \neg \varphi \)
Proof
l0
con3
con4
impbii l0 _