Theorem notbi

Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
Proof
id
l1
notbid _
id
con4bid _
impbii l1 _