Theorem con2bii

A contraposition inference. (Contributed by NM, 12-Mar-1993.)

Hypothesis
con2bii.1
\( \vdash \varphi \leftrightarrow \neg \psi \)
Conclusion
\( \vdash \psi \leftrightarrow \neg \varphi \)
Proof
l0
notnotb
\( \vdash \psi \leftrightarrow \neg \neg \psi \)
con2bii.1
\( \vdash \varphi \leftrightarrow \neg \psi \)
xchbinxr l0 _