Theorem bibif

Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)

Conclusion
\( \vdash \neg \psi \rightarrow (\varphi \leftrightarrow \psi \leftrightarrow \neg \varphi) \)
Proof
l0
nbn2
\( \vdash \neg \psi \rightarrow (\neg \varphi \leftrightarrow (\psi \leftrightarrow \varphi)) \)
bicom
\( \vdash \psi \leftrightarrow \varphi \leftrightarrow (\varphi \leftrightarrow \psi) \)
bitr2di l0 _