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 ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐶 )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 = 𝐶 ↔ 𝐵 = 𝐶 ) )
2 1 biimpar ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐶 )