Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20Aug1993)
Ref  Expression  

Assertion  equcom   ( x = y <> y = x ) 
Step  Hyp  Ref  Expression 

1  equcomi   ( x = y > y = x ) 

2  equcomi   ( y = x > x = y ) 

3  1 2  impbii   ( x = y <> y = x ) 