Theorem eqtr3 2160

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 2142	. 2 |- ( B = C <-> C = B )
2		eqtr 2158	. 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 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  eueq  2859  euind  2875  reuind  2893  preqsn  3710  eusv1  4381  funopg  5165  funinsn  5180  foco  5363  mpofun  5881  enq0tr  7266  lteupri  7449  elrealeu  7661  rereceu  7721  receuap  8454  xrltso  9612  xrlttri3  9613  iseqf1olemab  10293  fsumparts  11271  odd2np1  11606  exmidsbthrlem  13392