Description: Transitive law for class equality. Proposition 4.7(3) of TakeutiZaring p. 13. (Contributed by NM, 25Jan2004)
Ref  Expression  

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

1  eqeq1   ( A = B > ( A = C <> B = C ) ) 

2  1  biimpar   ( ( A = B /\ B = C ) > A = C ) 