Theorem eqtr3 2177

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

Assertion

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

Proof of Theorem eqtr3

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  eueq  2883  euind  2899  reuind  2917  preqsn  3738  eusv1  4411  funopg  5203  funinsn  5218  foco  5401  mpofun  5920  enq0tr  7348  lteupri  7531  elrealeu  7743  rereceu  7803  receuap  8537  xrltso  9696  xrlttri3  9697  iseqf1olemab  10381  fsumparts  11360  odd2np1  11756  exmidsbthrlem  13564