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

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

Proof of Theorem syl6eleq
StepHypRef Expression
1 syl6eleq.1 . 2  |-  ( ph  ->  A  e.  B )
2 syl6eleq.2 . . 3  |-  B  =  C
32a1i 10 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2359 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  syl6eleqr  2374  prid2g  3733  ndmfvrcl  5553  fnwelem  6230  tz7.48-1  6455  brwitnlem  6506  oeeulem  6599  dffi3  7184  cnfcom3lem  7406  alephgeom  7709  fpwwe2lem6  8257  canthwelem  8272  hargch  8299  r1wunlim  8359  eluzel2  10235  fznn0sub2  10825  fseq1p1m1  10857  exple1  11161  digit1  11235  bcval5  11330  bcpasc  11333  hashf1  11395  seqcoll  11401  seqcoll2  11402  swrdccat1  11460  swrdccat2  11461  splfv2a  11471  splval2  11472  cats1un  11476  caubnd  11842  limsupgre  11955  clim2ser  12128  clim2ser2  12129  iserex  12130  isermulc2  12131  iserle  12133  iserge0  12134  climub  12135  climserle  12136  isercolllem2  12139  isercolllem3  12140  isercoll  12141  isercoll2  12142  serf0  12153  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  sumeq2ii  12166  summolem3  12187  summolem2a  12188  fsum  12193  sum0  12194  fsumcl2lem  12204  fsumadd  12211  isumclim3  12222  isumadd  12230  fsump1i  12232  fsummulc2  12246  fsumrelem  12265  iserabs  12273  cvgcmp  12274  cvgcmpub  12275  cvgcmpce  12276  binom1dif  12291  isumshft  12298  isumsplit  12299  isumrpcl  12302  isumsup2  12305  climcndslem1  12308  climcndslem2  12309  climcnds  12310  arisum2  12319  trireciplem  12320  geoser  12325  geolim  12326  geo2lim  12331  cvgrat  12339  mertenslem1  12340  mertenslem2  12341  mertens  12342  efcvgfsum  12367  efcj  12373  effsumlt  12391  ruclem7  12514  bitsfzolem  12625  bitsfzo  12626  bitsfi  12628  bitsinv1lem  12632  bitsinv1  12633  bitsinvp1  12640  sadcp1  12646  sadadd  12658  sadass  12662  bitsres  12664  smupp1  12671  smuval2  12673  smupval  12679  smueqlem  12681  smumul  12684  algrp1  12744  phiprmpw  12844  crt  12846  phimullem  12847  eulerthlem2  12850  prmdiv  12853  pcpremul  12896  pcmpt  12940  pcfac  12947  pockthlem  12952  pockthg  12953  prmreclem2  12964  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  prmrec  12969  1arith  12974  vdwapun  13021  vdwlem1  13028  vdwlem2  13029  vdwlem3  13030  vdwlem6  13033  vdwlem8  13035  vdwlem10  13037  vdw  13041  imasvscafn  13439  xpsfrnel2  13467  oppccatid  13622  oppccomfpropd  13630  funcoppc  13749  invfuc  13848  hofcl  14033  yonedalem4c  14051  gsumwsubmcl  14461  gsumccat  14464  gsumwmhm  14467  mulgnnp1  14575  mulgnnsubcl  14579  mulgnn0z  14587  mulgnndir  14589  sylow1lem1  14909  lsmmod2  14985  lsmdisj2r  14994  efginvrel2  15036  efgsdmi  15041  efgsrel  15043  efgs1b  15045  efgsp1  15046  efgredleme  15052  efgredlemc  15054  efgcpbllemb  15064  frgpuplem  15081  mulgnn0di  15125  frgpnabllem1  15161  lt6abl  15181  cycsubgcyg  15187  gsumval3eu  15190  gsumval3  15191  gsumzcl  15195  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  dprd2da  15277  pgpfaclem1  15316  isirred  15481  lspprid2  15755  lspsnat  15898  lsppratlem1  15900  lsppratlem3  15902  lidl0cl  15964  lidlacl  15965  lidlnegcl  15966  lidlmcl  15969  psrbaglefi  16118  psrass23  16154  psr1bascl  16280  ply1basf  16283  cldrcl  16763  ordtbas  16922  iscnp2  16969  dis1stc  17225  ptbasfi  17276  ptpjopn  17306  ptclsg  17309  ptcnp  17316  kqtop  17436  reghmph  17484  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  tsmslem1  17811  imasdsf1olem  17937  blcvx  18304  xrhmeo  18444  cnrehmeo  18451  evth  18457  reparphti  18495  iscau4  18705  iscmet3lem1  18717  lmle  18727  pjthlem2  18802  ovollb2lem  18847  ovolunlem1a  18855  ovoliunlem1  18861  ovoliun2  18865  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem4  18879  iundisj2  18906  voliunlem1  18907  volsup  18913  ioombl1lem4  18918  uniioovol  18934  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  vitalilem5  18967  mbfimaopnlem  19010  mbflimsup  19021  mbfi1fseqlem3  19072  iblitg  19123  dvnp1  19274  cpncn  19285  dvlip2  19342  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumrlimge0  19377  dvfsumrlim2  19379  ftc1cn  19390  mpfind  19428  mpfpf1  19434  pf1mpf  19435  elplyd  19584  ply1termlem  19585  ply1term  19586  ply0  19590  plyeq0lem  19592  plyaddlem1  19595  plymullem1  19596  plyaddlem  19597  plymullem  19598  coeeulem  19606  plyco  19623  coeeq2  19624  coefv0  19629  coemulhi  19635  coemulc  19636  plycj  19658  dvply1  19664  vieta1lem2  19691  elqaalem2  19700  dvtaylp  19749  dvntaylp  19750  taylthlem1  19752  taylth  19754  ulmres  19767  ulmshftlem  19768  ulmshft  19769  ulmcau  19772  ulmdvlem1  19777  mtest  19781  pserulm  19798  psercn2  19799  psercnlem1  19801  psercn  19802  pserdvlem2  19804  abelthlem6  19812  abelth  19817  efif1olem1  19904  efif1olem3  19906  efif1olem4  19907  logcn  19994  advlogexp  20002  efopn  20005  cxpeq  20097  asinsin  20188  atantayl  20233  leibpilem2  20237  birthdaylem2  20247  birthdaylem3  20248  efrlim  20264  emcllem2  20290  emcllem5  20293  emcllem7  20295  harmonicbnd4  20304  fsumharmonic  20305  wilthlem2  20307  wilthlem3  20308  ftalem1  20310  ftalem2  20311  ftalem3  20312  ftalem5  20314  basellem2  20319  basellem3  20320  basellem5  20322  basellem8  20325  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  chpp1  20393  vma1  20404  ppiltx  20415  musum  20431  0sgmppw  20437  1sgmprm  20438  ppiublem2  20442  chtublem  20450  fsumvma2  20453  chpchtsum  20458  logexprlim  20464  bposlem5  20527  lgscllem  20542  lgsval2lem  20545  lgsval4a  20557  lgsneg  20558  lgsdir2lem3  20564  lgsdir2lem5  20566  lgsdir  20569  lgsdilem2  20570  lgsdi  20571  lgsne0  20572  lgseisenlem1  20588  lgsquadlem2  20594  chebbnd1lem1  20618  chtppilimlem1  20622  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasum2lem  20645  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0flb  20659  dchrisum0re  20662  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  selberg2lem  20699  logdivbnd  20705  pntrsumo1  20714  pntrsumbnd2  20716  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem6a  20731  pntlemj  20752  pntlemf  20754  ostth2lem3  20784  htthlem  21497  hhsscms  21856  shmodsi  21968  pjoc1i  22010  5oalem1  22233  mayete3i  22307  mayete3iOLD  22308  adj1  22513  ballotlemfrceq  23087  ssnnssfz  23277  iundisj2fi  23364  iundisj2f  23366  pnfneige0  23374  esumpcvgval  23446  esumpmono  23447  esumcvg  23454  indpreima  23608  orrvcval4  23665  orrvcoel  23666  orrvccel  23667  dmgmseqn0  23696  subfacp1lem1  23710  subfacp1lem5  23715  subfacp1lem6  23716  subfacval2  23718  erdszelem7  23728  cvxscon  23774  cvmliftlem5  23820  cvmliftlem7  23822  cvmliftlem10  23825  cvmliftlem13  23827  eupares  23899  eupap1  23900  eupath2lem3  23903  eupath2  23904  relexpsucr  24026  bdayelon  24334  imageval  24469  eedimeq  24526  axlowdimlem16  24585  bpolysum  24788  bpolydiflem  24789  fsumkthpow  24791  npincppr  25159  inposet  25278  exopcopn  25572  isray  26154  isside0  26164  aishp  26172  upixp  26403  sdclem2  26452  caushft  26477  ismtyres  26532  rrnmet  26553  rrndstprj1  26554  rrndstprj2  26555  rrncmslem  26556  rrnequiv  26559  iccbnd  26564  mapfzcons  26793  diophren  26896  irrapxlem1  26907  monotuz  27026  acongeq  27070  jm2.26lem3  27094  jm3.1lem2  27111  pw2f1ocnv  27130  psgnunilem4  27420  psgnghm  27437  matbas2i  27476  idomodle  27512  fcnre  27696  refsumcn  27701  rfcnnnub  27707  climsuselem1  27733  stoweidlem11  27760  stoweidlem15  27764  stoweidlem17  27766  stoweidlem20  27769  stoweidlem34  27783  stoweidlem47  27796  stoweidlem56  27805  stoweidlem59  27808  stoweidlem62  27811  stirlinglem5  27827  bnj1172  29031  bnj1245  29044  bnj1311  29054  bnj1450  29080  bnj1501  29097  osumcllem7N  30151  pexmidlem4N  30162  lcfrlem4  31735  lcfrlem5  31736  lcfrlem6  31737  lcfrlem16  31748  lcfrlem38  31770  mapdrvallem2  31835  mapdh8ab  31967  mapdh8ad  31969  mapdh8e  31974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator