MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eqelr Structured version   Unicode version

Theorem syl6eqelr 2564
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqelr.1  |-  ( ph  ->  B  =  A )
syl6eqelr.2  |-  B  e.  C
Assertion
Ref Expression
syl6eqelr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eqelr
StepHypRef Expression
1 syl6eqelr.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2475 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2563 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  wemoiso2  6767  releldm2  6831  mapprc  7421  ixpprc  7487  bren  7522  brdomg  7523  domssex  7675  mapen  7678  ssenen  7688  fodomfib  7796  fi0  7876  dffi3  7887  brwdom  7989  brwdomn0  7991  unxpwdom2  8010  ixpiunwdom  8013  tcmin  8168  rankonid  8243  rankr1id  8276  cardf2  8320  cardid2  8330  carduni  8358  fseqen  8404  acndom  8428  acndom2  8431  alephnbtwn  8448  cardcf  8628  cfeq0  8632  cflim2  8639  coftr  8649  infpssr  8684  hsmexlem5  8806  axdc3lem4  8829  fodomb  8900  ondomon  8934  gruina  9192  ioof  11618  hashbc  12464  hashfacen  12465  zsum  13499  fsum  13501  fsumcom2  13548  xpsfrnel2  14816  eqgen  16049  symgbas  16200  symgfisg  16289  dvdsr  17079  asplss  17749  aspsubrg  17751  psrval  17782  clsf  19315  restco  19431  subbascn  19521  is2ndc  19713  ptbasin2  19814  ptbas  19815  indishmph  20034  ufldom  20198  cnextfres  20303  ussid  20498  icopnfcld  21010  cnrehmeo  21188  csscld  21424  clsocv  21425  itg2gt0  21902  dvmptadd  22098  dvmptmul  22099  dvmptco  22110  logcn  22756  selberglem1  23458  wlkcompim  24202  wlkelwrd  24206  clwlkcompim  24440  hmopidmchi  26746  ctex  27203  sigagensiga  27781  dya2iocbrsiga  27886  dya2icobrsiga  27887  fprod  28650  fprodcom2  28691  fnessref  29765  unirep  29806  indexdom  29828  pwslnmlem0  30641  mendval  30737  dvsubf  31242  fperdvper  31248  dvdivf  31252  itgsinexplem1  31271  stirlinglem7  31380  fouriersw  31532  dicfnN  35980
  Copyright terms: Public domain W3C validator