This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = B ∧ B = C → A = C

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ A = B → A = C ↔ B = C
2 1 biimpar ⊢ A = B ∧ B = C → A = C