Metamath Proof Explorer


Theorem eqtr

Description: Transitive law for class equality. Proposition 4.7(3) of TakeutiZaring p. 13. (Contributed by NM, 25-Jan-2004)

Ref Expression
Assertion eqtr A=BB=CA=C

Proof

Step Hyp Ref Expression
1 eqeq1 A=BA=CB=C
2 1 biimpar A=BB=CA=C