Theorem con4bii

A contraposition inference. (Contributed by NM, 21-May-1994.)

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