Theorem con1bii

A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)

Hypothesis
con1bii.1
\( \vdash \neg \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \neg \psi \leftrightarrow \varphi \)
Proof
l0
notnotb
\( \vdash \varphi \leftrightarrow \neg \neg \varphi \)
con1bii.1
\( \vdash \neg \varphi \leftrightarrow \psi \)
xchbinx l0 _
bicomi _