Metamath Proof Explorer

Theorem equcom

Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993)

Ref Expression
Assertion equcom 
|- ( x = y <-> y = x )

Proof

Step Hyp Ref Expression
1 equcomi 
 |-  ( x = y -> y = x )
2 equcomi 
 |-  ( y = x -> x = y )
3 1 2 impbii 
 |-  ( x = y <-> y = x )