Theorem
equcom
Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
Conclusion
\( \vdash x' = y' \leftrightarrow y' = x' \)
Proof
l0
equcomi
equcomi
impbii
l0
_
This is the content in the right pane.