Theorem nbn3

Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)

Hypothesis
nbn3.1
\( \vdash \varphi \)
Conclusion
\( \vdash \neg \psi \leftrightarrow (\psi \leftrightarrow \neg \varphi) \)
Proof
nbn3.1
notnoti _
nbn _