Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27Dec1993) Allow shortening of eqeq2 . (Revised by Wolf Lammen, 19Nov2019)
Ref  Expression  

Hypothesis  eqeq2d.1   ( ph > A = B ) 

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

1  eqeq2d.1   ( ph > A = B ) 

2  1  eqeq1d   ( ph > ( A = C <> B = C ) ) 
3  eqcom   ( C = A <> A = C ) 

4  eqcom   ( C = B <> B = C ) 

5  2 3 4  3bitr4g   ( ph > ( C = A <> C = B ) ) 