Theorem eqtr3 2258

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 2240	. 2 |- ( B = C <-> C = B )
2		eqtr 2256	. 2 |- ( ( A = C /\ C = B ) -> A = B )
3	1, 2	sylan2b 287	1 |- ( ( A = C /\ B = C ) -> A = B )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eueq  2997  euind  3013  reuind  3031  ssprsseq  3877  preqsn  3900  eusv1  4600  funopg  5414  funinsn  5433  foco  5629  funopdmsn  5898  mpofun  6193  enq0tr  7807  lteupri  7990  elrealeu  8202  rereceu  8262  receuap  9007  xrltso  10215  xrlttri3  10216  iseqf1olemab  10960  fsumparts  12262  odd2np1  12665  grpinveu  13902  exmidsbthrlem  17273