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  4598  funopg  5411  funinsn  5430  foco  5626  funopdmsn  5895  mpofun  6190  enq0tr  7801  lteupri  7984  elrealeu  8196  rereceu  8256  receuap  8999  xrltso  10198  xrlttri3  10199  iseqf1olemab  10939  fsumparts  12237  odd2np1  12640  grpinveu  13843  exmidsbthrlem  17067