Metamath Proof Explorer

Theorem eqtr3

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005)

Ref Expression
Assertion eqtr3 
|- ( ( A = C /\ B = C ) -> A = B )

Proof

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