Theorem eqtr3 2225

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 2207	. 2 |- ( B = C <-> C = B )
2		eqtr 2223	. 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 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  eueq  2944  euind  2960  reuind  2978  preqsn  3816  eusv1  4500  funopg  5306  funinsn  5324  foco  5511  funopdmsn  5766  mpofun  6049  enq0tr  7549  lteupri  7732  elrealeu  7944  rereceu  8004  receuap  8744  xrltso  9920  xrlttri3  9921  iseqf1olemab  10649  fsumparts  11814  odd2np1  12217  grpinveu  13403  exmidsbthrlem  15998