Theorem
bicom1
Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012.)
Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\psi \leftrightarrow \varphi) \)
Proof
l0
biimpr
biimp
impbid
l0
_
This is the content in the right pane.