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 
|- ( ( A = B /\ A = C ) -> B = C )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( A = B <-> B = A )
2 eqtr 
 |-  ( ( B = A /\ A = C ) -> B = C )
3 1 2 sylanb 
 |-  ( ( A = B /\ A = C ) -> B = C )