Description: A transitive law for class equality. (Contributed by NM, 20May2005)
Ref  Expression  

Assertion  eqtr3   ( ( A = C /\ B = C ) > A = B ) 
Step  Hyp  Ref  Expression 

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

2  eqtr   ( ( A = C /\ C = B ) > A = B ) 

3  1 2  sylan2b   ( ( A = C /\ B = C ) > A = B ) 