Theorem eqtr3 2643

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 2629	. 2 |- ( B = C <-> C = B )
2		eqtr 2641	. 2 |- ( ( A = C /\ C = B ) -> A = B )
3	1, 2	sylan2b 492	1 |- ( ( A = C /\ B = C ) -> A = B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  neneor  2893  eueq  3378  euind  3393  reuind  3411  ssprsseq  4357  prnebg  4389  preqsnOLD  4394  3elpr2eq  4435  eusv1  4860  restidsingOLD  5459  xpcan  5570  xpcan2  5571  funopg  5922  foco  6125  funopdmsn  6415  funsndifnop  6416  mpt2fun  6762  wfr3g  7413  oawordeulem  7634  ixpfi2  8264  wemapso2lem  8457  isf32lem2  9176  fpwwe2lem13  9464  1re  10039  receu  10672  xrlttri  11972  injresinjlem  12588  cshwsexa  13570  fsumparts  14538  odd2np1  15065  prmreclem2  15621  divsfval  16207  isprs  16930  psrn  17209  grpinveu  17456  symgextf1  17841  symgfixf1  17857  efgrelexlemb  18163  lspextmo  19056  evlseu  19516  tgcmp  21204  sqf11  24865  dchrisumlem2  25179  axlowdimlem15  25836  axcontlem2  25845  wlksoneq1eq2  26560  spthonepeq  26648  uspgrn2crct  26700  wwlksnextinj  26794  frgrwopreglem5lem  27184  numclwlk1lem2f1  27227  nsnlplig  27333  nsnlpligALT  27334  grpoinveu  27373  5oalem4  28516  rnbra  28966  xreceu  29630  bnj594  30982  bnj953  31009  frr3g  31779  sltsolem1  31826  nocvxminlem  31893  fnsingle  32026  funimage  32035  funtransport  32138  funray  32247  funline  32249  hilbert1.2  32262  lineintmo  32264  bj-bary1  33162  poimirlem13  33422  poimirlem14  33423  poimirlem17  33426  poimirlem27  33436  prtlem11  34151  prter2  34166  cdleme  35848  kelac2lem  37634  frege124d  38053  2ffzoeq  41338  sprsymrelf1lem  41741