Theorem notbii

Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis
notbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \neg \varphi \leftrightarrow \neg \psi \)
Proof
l0
notbii.1
\( \vdash \varphi \leftrightarrow \psi \)
notbi
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
mpbi l0 _