Theorem con2bi

Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (Contributed by NM, 15-Apr-1995.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)

Conclusion
\( \vdash \varphi \leftrightarrow \neg \psi \leftrightarrow (\psi \leftrightarrow \neg \varphi) \)
Proof
l0
notbi
\( \vdash \varphi \leftrightarrow \neg \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \neg \psi) \)
notnotb
l2
bibi2i _
\( \vdash \neg \varphi \leftrightarrow \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \neg \psi) \)
bicom
\( \vdash \neg \varphi \leftrightarrow \psi \leftrightarrow (\psi \leftrightarrow \neg \varphi) \)
3bitr2i l0 l2 _