Theorem bicom

Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\psi \leftrightarrow \varphi) \)
Proof
l0
bicom1
bicom1
impbii l0 _