Theorem eqtr3 2107

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 2090	. 2 |- ( B = C <-> C = B )
2		eqtr 2105	. 2 |- ( ( A = C /\ C = B ) -> A = B )
3	1, 2	sylan2b 281	1 |- ( ( A = C /\ B = C ) -> A = B )

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  eueq  2786  euind  2802  reuind  2820  preqsn  3619  eusv1  4274  funopg  5048  funinsn  5063  foco  5243  mpt2fun  5747  enq0tr  6993  lteupri  7176  elrealeu  7367  rereceu  7424  receuap  8138  xrltso  9266  xrlttri3  9267  iseqf1olemab  9918  fsumparts  10864  odd2np1  11151  exmidsbthrlem  11912