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

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( B = C -> ( A = B <-> A = C ) )
2 1 biimparc 
 |-  ( ( A = C /\ B = C ) -> A = B )