Theorem notbid

Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)

Hypothesis
notbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\neg \psi \leftrightarrow \neg \chi) \)
Proof
l0
notbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l1
notnotb
\( \vdash \psi \leftrightarrow \neg \neg \psi \)
notnotb
\( \vdash \chi \leftrightarrow \neg \neg \chi \)
3bitr3g l0 l1 _
con4bid _