Theorem bicomd

Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis
bicomd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \psi) \)
Proof
l0
bicomd.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bicom
\( \vdash \psi \leftrightarrow \chi \leftrightarrow (\chi \leftrightarrow \psi) \)
sylib l0 _