Description: Equality implies equivalence of equalities. (Contributed by NM, 26May1993) (Proof shortened by Wolf Lammen, 19Nov2019)
Ref  Expression  

Assertion  eqeq2   ( A = B > ( C = A <> C = B ) ) 
Step  Hyp  Ref  Expression 

1  id   ( A = B > A = B ) 

2  1  eqeq2d   ( A = B > ( C = A <> C = B ) ) 