Metamath Proof Explorer

Theorem eqtr3OLD

Description: Obsolete version of eqtr3 as of 24-Oct-2024. (Contributed by NM, 20-May-2005) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion eqtr3OLD 
|- ( ( 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 )