Theorem eqtr3 2101

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 2084	. 2 |- ( B = C <-> C = B )
2		eqtr 2099	. 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 1285

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

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

This theorem is referenced by:  eueq  2764  euind  2780  reuind  2796  preqsn  3575  eusv1  4210  funopg  4964  funinsn  4979  foco  5147  mpt2fun  5634  enq0tr  6686  lteupri  6869  elrealeu  7060  rereceu  7117  receuap  7826  xrltso  8947  xrlttri3  8948  odd2np1  10417