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

Theorem syl6eleq 2521
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 11 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2513 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    e. wcel 1869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-cleq 2415  df-clel 2418
This theorem is referenced by:  syl6eleqr  2522  3eltr3g  2527  prid2g  4105  ndmfvrcl  5904  fnwelem  6920  tz7.48-1  7166  brwitnlem  7215  oeeulem  7308  dffi3  7949  cnfcom3lem  8211  alephgeom  8515  fpwwe2lem6  9062  canthwelem  9077  hargch  9100  r1wunlim  9164  eluzel2  11166  fseq1p1m1  11870  fznn0sub2  11899  nn0split  11908  exple1  12333  digit1  12407  bcval5  12504  bcpasc  12507  hashf1  12619  seqcoll  12626  seqcoll2  12627  ccatrn  12731  swrdccat1  12809  swrdccat2  12810  cats1un  12828  splfv2a  12859  splval2  12860  caubnd  13415  limsupgre  13535  limsupgreOLD  13536  clim2ser  13711  clim2ser2  13712  iserex  13713  isermulc2  13714  iserle  13716  iserge0  13717  climub  13718  climserle  13719  isercolllem2  13722  isercolllem3  13723  isercoll  13724  isercoll2  13725  serf0  13740  iseraltlem2  13742  iseraltlem3  13743  iseralt  13744  sumeq2ii  13752  summolem3  13773  summolem2a  13774  fsum  13779  sum0  13780  fsumcl2lem  13790  fsumadd  13798  isumclim3  13813  isumadd  13821  fsump1i  13823  fsummulc2  13838  fsumrelem  13860  iserabs  13868  cvgcmp  13869  cvgcmpub  13870  cvgcmpce  13871  binom1dif  13884  isumshft  13890  isumsplit  13891  isumrpcl  13894  isumsup2  13897  climcndslem1  13900  climcndslem2  13901  climcnds  13902  arisum2  13912  trireciplem  13913  geoser  13918  geolim  13919  geo2lim  13924  cvgrat  13932  mertenslem1  13933  mertenslem2  13934  mertens  13935  clim2prod  13937  clim2div  13938  ntrivcvgfvn0  13948  ntrivcvgtail  13949  prodeq2ii  13960  prodmolem3  13980  prodmolem2a  13981  fprod  13988  fprodntriv  13989  fprodss  13995  fprodser  13996  fprodcl2lem  13997  fprodmul  14007  fproddiv  14008  fprodabs  14021  fprodeq0  14022  fprodn0  14026  iprodclim3  14046  iprodmul  14049  fallfacfwd  14082  0fallfac  14083  binomfallfaclem2  14086  fallfacval4  14089  bpolysum  14099  bpolydiflem  14100  fsumkthpow  14102  efcvgfsum  14133  efcj  14139  fprodefsum  14142  effsumlt  14158  ruclem7  14281  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsfi  14404  bitsinv1lem  14408  bitsinv1  14409  bitsinvp1  14416  sadcp1  14422  sadadd  14434  sadass  14438  bitsres  14440  smupp1  14447  smuval2  14449  smupval  14455  smueqlem  14457  smumul  14460  algrp1  14526  phiprmpw  14717  crt  14719  phimullem  14720  eulerthlem2  14723  prmdiv  14726  pcpremul  14786  pcmpt  14830  pcfac  14837  pockthlem  14842  pockthg  14843  prmreclem2  14854  prmreclem3  14855  prmreclem4  14856  prmreclem5  14857  prmreclem6  14858  prmrec  14859  1arith  14864  vdwapun  14917  vdwlem1  14924  vdwlem2  14925  vdwlem3  14926  vdwlem6  14929  vdwlem8  14931  vdwlem10  14933  vdw  14937  imasvscafn  15436  xpsfrnel2  15464  oppccatid  15617  oppccomfpropd  15625  brcic  15696  funcoppc  15773  invfuc  15872  hofcl  16137  yonedalem4c  16155  gsumwsubmcl  16615  gsumccat  16618  gsumwmhm  16622  mulgnnp1  16759  mulgnnsubcl  16763  mulgnn0z  16771  mulgnndir  16773  psgnunilem4  17131  psgnran  17149  sylow1lem1  17243  lsmmod2  17319  lsmdisj2r  17328  efginvrel2  17370  efgsdmi  17375  efgsrel  17377  efgs1b  17379  efgsp1  17380  efgredleme  17386  efgredlemc  17388  efgcpbllemb  17398  frgpuplem  17415  mulgnn0di  17459  frgpnabllem1  17502  lt6abl  17522  cycsubgcyg  17528  gsumval3eu  17531  gsumval3  17534  gsumzcl2  17537  gsumzaddlem  17547  gsumconst  17560  gsumzmhm  17563  gsumzoppg  17570  telgsumfz0s  17614  dprdwd  17636  dprd2da  17668  pgpfaclem1  17707  srgbinom  17771  isirred  17920  lspprid2  18214  lspsnat  18361  lsppratlem1  18363  lsppratlem3  18365  lidl0cl  18428  lidlacl  18429  lidlnegcl  18430  lidlmcl  18434  psrbaglefi  18589  psrass23l  18625  psrass23  18627  mplcoe5lem  18684  mpfind  18752  psr1bascl  18786  ply1basf  18788  gsummoncoe1  18891  lply1binom  18893  lply1binomsc  18894  mpfpf1  18932  pf1mpf  18933  evl1scvarpw  18944  psgnghm  19140  matbas2i  19439  matecld  19443  matgsum  19454  mpt2matmul  19463  dmatmul  19514  1mavmul  19565  mdetleib2  19605  m1detdiag  19614  marep01ma  19677  smadiadetlem4  19686  slesolinv  19697  pmatcollpw3fi1lem1  19802  chpscmat  19858  chpscmatgsumbin  19860  chp0mat  19862  chpidmat  19863  chfacfisf  19870  chfacfisfcpmat  19871  chfacfpmmulgsum2  19881  cldrcl  20033  ordtbas  20200  iscnp2  20247  dis1stc  20506  ptbasfi  20588  ptpjopn  20619  ptclsg  20622  ptcnp  20629  kqtop  20752  reghmph  20800  ptcmplem2  21060  ptcmplem3  21061  ptcmplem4  21062  tsmslem1  21135  utop2nei  21257  isucn2  21286  cuspcvg  21308  cnextucn  21310  imasdsf1olem  21380  blcvx  21808  xrhmeo  21966  cnrehmeo  21973  evth  21979  reparphti  22020  iscau4  22241  iscmet3lem1  22253  lmle  22263  rrxfsupp  22348  pjthlem2  22384  ovollb2lem  22433  ovolunlem1a  22441  ovoliunlem1  22447  ovoliun2  22451  ovolscalem1  22458  ovolicc1  22461  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  iundisj2  22494  voliunlem1  22495  volsup  22501  ioombl1lem4  22506  uniioovol  22528  uniioombllem3  22535  uniioombllem4  22536  uniioombllem6  22538  vitalilem5  22562  mbfimaopnlem  22603  mbflimsup  22615  mbflimsupOLD  22616  mbfi1fseqlem3  22667  iblitg  22718  dvnp1  22871  cpncn  22882  dvlip2  22939  dvfsumlem2  22971  dvfsumlem3  22972  dvfsumrlimge0  22974  dvfsumrlim2  22976  ftc1cn  22987  elplyd  23148  ply1termlem  23149  ply1term  23150  ply0  23154  plyeq0lem  23156  plyaddlem1  23159  plymullem1  23160  plyaddlem  23161  plymullem  23162  coeeulem  23170  plyco  23187  coeeq2  23188  coefv0  23194  coemulhi  23200  coemulc  23201  plycj  23223  dvply1  23229  vieta1lem2  23256  elqaalem2  23265  elqaalem2OLD  23268  dvtaylp  23317  dvntaylp  23318  taylthlem1  23320  taylth  23322  ulmres  23335  ulmshftlem  23336  ulmshft  23337  ulmcau  23342  ulmdvlem1  23347  mtest  23351  mtestbdd  23352  pserulm  23369  psercn2  23370  psercnlem1  23372  psercn  23373  pserdvlem2  23375  abelthlem6  23383  abelth  23388  efif1olem1  23483  efif1olem3  23485  efif1olem4  23486  logcn  23584  advlogexp  23592  efopn  23595  cxpeq  23689  asinsin  23810  atantayl  23855  leibpilem2  23859  birthdaylem2  23870  birthdaylem3  23871  efrlim  23887  emcllem2  23914  emcllem5  23917  emcllem7  23919  harmonicbnd4  23928  fsumharmonic  23929  lgamgulm2  23953  lgamcvglem  23957  lgamcvg2  23972  gamcvg2lem  23976  wilthlem2  23986  wilthlem3  23987  ftalem1  23989  ftalem2  23990  ftalem3  23991  ftalem5  23993  ftalem5OLD  23995  basellem2  24000  basellem3  24001  basellem5  24003  basellem8  24006  ppiprm  24070  ppinprm  24071  chtprm  24072  chtnprm  24073  chpp1  24074  vma1  24085  ppiltx  24096  musum  24112  0sgmppw  24118  1sgmprm  24119  ppiublem2  24123  chtublem  24131  fsumvma2  24134  chpchtsum  24139  logexprlim  24145  bposlem5  24208  lgscllem  24223  lgsval2lem  24226  lgsval4a  24238  lgsneg  24239  lgsdir2lem3  24245  lgsdir2lem5  24247  lgsdir  24250  lgsdilem2  24251  lgsdi  24252  lgsne0  24253  lgseisenlem1  24269  lgsquadlem2  24275  chebbnd1lem1  24299  chtppilimlem1  24303  rplogsumlem2  24315  rpvmasumlem  24317  dchrisumlem1  24319  dchrisumlem2  24320  dchrmusum2  24324  dchrvmasum2lem  24326  dchrvmasumiflem1  24331  dchrisum0flblem1  24338  dchrisum0flblem2  24339  dchrisum0flb  24340  dchrisum0re  24343  dchrisum0lem1b  24345  dchrisum0lem1  24346  dchrisum0lem2a  24347  dchrisum0lem2  24348  dchrisum0lem3  24349  mudivsum  24360  mulogsum  24362  mulog2sumlem2  24365  selberg2lem  24380  logdivbnd  24386  pntrsumo1  24395  pntrsumbnd2  24397  pntrlog2bndlem2  24408  pntrlog2bndlem4  24410  pntrlog2bndlem6a  24412  pntlemj  24433  pntlemf  24435  ostth2lem3  24465  tglngne  24587  ltgseg  24633  eedimeq  24920  axlowdimlem16  24979  ebtwntg  25004  eupares  25695  eupap1  25696  eupath2lem3  25699  eupath2  25700  htthlem  26562  hhsscms  26922  shmodsi  27034  pjoc1i  27076  5oalem1  27299  mayete3i  27373  adj1  27578  iundisj2f  28196  fcnvgreu  28271  ssnnssfz  28367  iundisj2fi  28373  fz1fzo0m1  28379  pmtrto1cl  28614  psgnfzto1stlem  28615  fzto1st1  28617  1smat1  28632  submateqlem2  28636  lmatfval  28642  mdetlap1  28654  madjusmdetlem1  28655  madjusmdetlem2  28656  madjusmdetlem3  28657  madjusmdetlem4  28658  pnfneige0  28759  pl1cn  28763  rrhqima  28820  indpreima  28848  esumfzf  28892  esumpcvgval  28901  esumpmono  28902  esumcvg  28909  ldgenpisyslem1  28987  ldgenpisys  28990  measbase  29021  dya2iocnei  29106  oddpwdc  29189  eulerpartlems  29195  eulerpartlemb  29203  sseqf  29227  fibp1  29236  orrvcval4  29299  orrvcoel  29300  orrvccel  29301  ballotlem2  29323  ballotlemfrceq  29363  ballotlemfrceqOLD  29401  signsplypnf  29441  signswch  29452  signstf0  29459  signstfvn  29460  signstfvneq0  29463  signstfvcl  29464  signstfveq0  29468  signsvfn  29473  bnj1172  29812  bnj1245  29825  bnj1311  29835  bnj1450  29861  bnj1501  29878  subfacp1lem1  29904  subfacp1lem5  29909  subfacp1lem6  29910  subfacval2  29912  erdszelem7  29922  cvxscon  29968  cvmliftlem5  30014  cvmliftlem7  30016  cvmliftlem10  30019  cvmliftlem13  30021  mrsubvrs  30162  msubrn  30169  msubco  30171  msubvrs  30200  bdayelon  30568  imageval  30696  fwddifnp1  30931  icoreunrn  31709  istoprelowl  31710  poimirlem3  31863  poimirlem4  31864  poimirlem6  31866  poimirlem7  31867  poimirlem8  31868  poimirlem12  31872  poimirlem15  31875  poimirlem16  31876  poimirlem17  31877  poimirlem18  31878  poimirlem19  31879  poimirlem20  31880  poimirlem21  31881  poimirlem22  31882  poimirlem23  31883  poimirlem24  31884  poimirlem25  31885  poimirlem26  31886  poimirlem27  31887  poimirlem28  31888  poimirlem29  31889  poimirlem31  31891  mblfinlem2  31898  ftc1cnnc  31936  upixp  31976  sdclem2  31991  caushft  32010  ismtyres  32060  rrnmet  32081  rrndstprj1  32082  rrndstprj2  32083  rrncmslem  32084  rrnequiv  32087  iccbnd  32092  osumcllem7N  33452  pexmidlem4N  33463  lcfrlem4  35038  lcfrlem5  35039  lcfrlem6  35040  lcfrlem16  35051  lcfrlem38  35073  mapdrvallem2  35138  mapdh8ab  35270  mapdh8ad  35272  mapdh8e  35277  mapfzcons  35483  diophren  35581  irrapxlem1  35592  monotuz  35715  acongeq  35759  jm2.26lem3  35782  jm3.1lem2  35799  pw2f1ocnv  35818  idomodle  35996  trclfvdecomr  36186  imo72b2lem1  36478  dvgrat  36525  cvgdvgrat  36526  hashnzfz2  36534  fcnre  37213  refsumcn  37218  rfcnnnub  37224  disjf1o  37322  disjinfi  37324  ssuzfz  37420  climsuselem1  37512  limcperiod  37534  sumnnodd  37536  lptioo2cn  37552  lptioo1cn  37553  cncfshift  37577  cncfperiod  37582  cncfshiftioo  37596  fperdvper  37616  dvnmptdivc  37639  dvnmul  37644  dvmptfprod  37646  dvnprodlem3  37649  stoweidlem11  37697  stoweidlem15  37701  stoweidlem17  37703  stoweidlem20  37706  stoweidlem34  37721  stoweidlem35  37722  stoweidlem46  37733  stoweidlem47  37734  stoweidlem56  37743  stoweidlem59  37746  stoweidlem62  37749  stoweidlem62OLD  37750  stirlinglem5  37766  stirlinglem14  37775  dirkertrigeqlem2  37787  dirkertrigeqlem3  37788  fourierdlem11  37806  fourierdlem15  37810  fourierdlem16  37811  fourierdlem21  37816  fourierdlem22  37817  fourierdlem25  37820  fourierdlem48  37844  fourierdlem52  37848  fourierdlem54  37850  fourierdlem58  37854  fourierdlem62  37858  fourierdlem64  37860  fourierdlem65  37861  fourierdlem69  37865  fourierdlem70  37866  fourierdlem71  37867  fourierdlem73  37869  fourierdlem80  37876  fourierdlem81  37877  fourierdlem83  37879  fourierdlem92  37888  fourierdlem93  37889  fourierdlem97  37893  fourierdlem103  37899  fourierdlem104  37900  fourierdlem112  37908  fourierdlem113  37909  fouriercnp  37916  fouriersw  37921  elaa2lem  37923  elaa2lemOLD  37924  etransclem4  37929  etransclem7  37932  etransclem10  37935  etransclem14  37939  etransclem15  37940  etransclem24  37949  etransclem25  37950  etransclem31  37956  etransclem32  37957  etransclem35  37960  etransclem44  37969  etransclem46  37971  prsal  37986  sge0tsms  38016  sge0fodjrnlem  38052  sge0isum  38063  iundjiunlem  38082  iundjiun  38083  meadjiunlem  38088  meaiunlelem  38091  caragensplit  38106  carageneld  38108  carageniuncllem1  38127  caratheodorylem1  38132  caratheodorylem2  38133  hoicvr  38151  elmod2  38442  ssnn0ssfz  39436  zlmodzxzscm  39444  rmsupp0  39459  lincsum  39528  lincscm  39529  lindslinindimp2lem4  39560  lincresunit3  39580  elbigofrcl  39667  aacllem  39846
  Copyright terms: Public domain W3C validator