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 )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  eueq  2997  euind  3013  reuind  3031  ssprsseq  3872  preqsn  3895  eusv1  4593  funopg  5406  funinsn  5425  foco  5621  funopdmsn  5886  mpofun  6180  enq0tr  7791  lteupri  7974  elrealeu  8186  rereceu  8246  receuap  8989  xrltso  10177  xrlttri3  10178  iseqf1olemab  10917  fsumparts  12215  odd2np1  12618  grpinveu  13820  exmidsbthrlem  16972