Metamath Proof Explorer

Theorem eqtr3

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005) (Proof shortened by Wolf Lammen, 24-Oct-2024)

Ref Expression
Assertion eqtr3 ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )

Proof

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