Description: A transitive law for class equality. (Contributed by NM, 20May2005) (Proof shortened by Andrew Salmon, 25May2011)
Ref  Expression  

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

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

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

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