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

Theorem syl6eqelr 2526
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 2442 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqelr.2 . 2  |-  B  e.  C
42, 3syl6eqel 2525 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eusvnfb  4720  wemoiso2  6080  releldm2  6398  mapprc  7023  ixpprc  7084  bren  7118  brdomg  7119  domssex  7269  mapen  7272  ssenen  7282  fodomfib  7387  fi0  7426  dffi3  7437  brwdom  7536  brwdomn0  7538  unxpwdom2  7557  ixpiunwdom  7560  tcmin  7681  tz9.12lem1  7714  rankonid  7756  rankr1id  7789  cardf2  7831  cardid2  7841  carduni  7869  fseqen  7909  acndom  7933  acndom2  7936  alephnbtwn  7953  cardcf  8133  cfeq0  8137  cflim2  8144  coftr  8154  infpssr  8189  hsmexlem5  8311  axdc3lem4  8334  fodomb  8405  ondomon  8439  gruina  8694  ioof  11003  hashbc  11703  hashfacen  11704  fsum  12515  fsumcom2  12559  xpsfrnel2  13791  eqgen  14994  symgbas  15096  dvdsr  15752  asplss  16389  aspsubrg  16391  psrval  16430  clsf  17113  restco  17229  subbascn  17319  is2ndc  17510  ptbasin2  17611  ptbas  17612  indishmph  17831  ufldom  17995  cnextfres  18100  ussid  18291  icopnfcld  18803  cnrehmeo  18979  csscld  19204  clsocv  19205  itg2gt0  19653  dvmptadd  19847  dvmptmul  19848  dvmptco  19859  logcn  20539  selberglem1  21240  hmopidmchi  23655  ctex  24101  sigagensiga  24525  dya2iocbrsiga  24626  dya2icobrsiga  24627  fprod  25268  fprodcom2  25309  fnessref  26374  indexdom  26437  pwslnmlem0  27171  symgfisg  27387  mendval  27469  itgsinexplem1  27725  stirlinglem7  27806  wlkelwrd  28296  wlkcompim  28303  dicfnN  31982
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2430  df-clel 2433
  Copyright terms: Public domain W3C validator