Description: Deduction from commutative law for class equality. (Contributed by NM, 15Aug1994) Allow shortening of eqcom . (Revised by Wolf Lammen, 19Nov2019)
Ref  Expression  

Hypothesis  eqcomd.1   ( ph > A = B ) 

Assertion  eqcomd   ( ph > B = A ) 
Step  Hyp  Ref  Expression 

1  eqcomd.1   ( ph > A = B ) 

2  eqid   A = A 

3  1  eqeq1d   ( ph > ( A = A <> B = A ) ) 
4  2 3  mpbii   ( ph > B = A ) 