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

Theorem syl6eqelr 2532
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 2448 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2531 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439
This theorem is referenced by:  wemoiso2  6568  releldm2  6629  mapprc  7223  ixpprc  7289  bren  7324  brdomg  7325  domssex  7477  mapen  7480  ssenen  7490  fodomfib  7596  fi0  7675  dffi3  7686  brwdom  7787  brwdomn0  7789  unxpwdom2  7808  ixpiunwdom  7811  tcmin  7966  rankonid  8041  rankr1id  8074  cardf2  8118  cardid2  8128  carduni  8156  fseqen  8202  acndom  8226  acndom2  8229  alephnbtwn  8246  cardcf  8426  cfeq0  8430  cflim2  8437  coftr  8447  infpssr  8482  hsmexlem5  8604  axdc3lem4  8627  fodomb  8698  ondomon  8732  gruina  8990  ioof  11392  hashbc  12211  hashfacen  12212  zsum  13200  fsum  13202  fsumcom2  13246  xpsfrnel2  14508  eqgen  15739  symgbas  15890  symgfisg  15979  dvdsr  16743  asplss  17405  aspsubrg  17407  psrval  17434  clsf  18657  restco  18773  subbascn  18863  is2ndc  19055  ptbasin2  19156  ptbas  19157  indishmph  19376  ufldom  19540  cnextfres  19645  ussid  19840  icopnfcld  20352  cnrehmeo  20530  csscld  20766  clsocv  20767  itg2gt0  21243  dvmptadd  21439  dvmptmul  21440  dvmptco  21451  logcn  22097  selberglem1  22799  hmopidmchi  25560  ctex  26013  sigagensiga  26589  dya2iocbrsiga  26695  dya2icobrsiga  26696  fprod  27459  fprodcom2  27500  fnessref  28570  unirep  28611  indexdom  28633  pwslnmlem0  29449  mendval  29545  itgsinexplem1  29799  stirlinglem7  29880  wlkelwrd  30285  wlkcompim  30292  clwlkcompim  30432  dicfnN  34833
  Copyright terms: Public domain W3C validator