Theorem bicomi

Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis
bicomi.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \psi \leftrightarrow \varphi \)
Proof
l0
bicomi.1
\( \vdash \varphi \leftrightarrow \psi \)
bicom1
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\psi \leftrightarrow \varphi) \)
ax-mp l0 _