Metamath Proof Explorer


Theorem eqtr2

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion eqtr2 ( ( 𝐴 = 𝐵𝐴 = 𝐶 ) → 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 eqcom ( 𝐴 = 𝐵𝐵 = 𝐴 )
2 eqtr ( ( 𝐵 = 𝐴𝐴 = 𝐶 ) → 𝐵 = 𝐶 )
3 1 2 sylanb ( ( 𝐴 = 𝐵𝐴 = 𝐶 ) → 𝐵 = 𝐶 )