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

Theorem syl6eleq 2740
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eleq.1 (𝜑𝐴𝐵)
syl6eleq.2 𝐵 = 𝐶
Assertion
Ref Expression
syl6eleq (𝜑𝐴𝐶)

Proof of Theorem syl6eleq
StepHypRef Expression
1 syl6eleq.1 . 2 (𝜑𝐴𝐵)
2 syl6eleq.2 . . 3 𝐵 = 𝐶
32a1i 11 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2732 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  syl6eleqr  2741  3eltr3g  2746  prid2g  4328  ndmfvrcl  6257  fnwelem  7337  tz7.48-1  7583  brwitnlem  7632  oeeulem  7726  dffi3  8378  cnfcom3lem  8638  alephgeom  8943  fpwwe2lem6  9495  canthwelem  9510  hargch  9533  r1wunlim  9597  eluzel2  11730  fseq1p1m1  12452  fznn0sub2  12485  nn0split  12493  fz1fzo0m1  12555  exple1  12960  digit1  13038  bcval5  13145  bcpasc  13148  hashf1  13279  seqcoll  13286  seqcoll2  13287  ccatrn  13407  swrdccat1  13503  swrdccat2  13504  cats1un  13521  splfv2a  13553  splval2  13554  caubnd  14142  limsupgre  14256  clim2ser  14429  clim2ser2  14430  iserex  14431  isermulc2  14432  iserle  14434  iserge0  14435  climub  14436  climserle  14437  isercolllem2  14440  isercolllem3  14441  isercoll  14442  isercoll2  14443  serf0  14455  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  sumeq2ii  14467  summolem3  14489  summolem2a  14490  fsum  14495  sum0  14496  fsumcl2lem  14506  fsumadd  14514  isumclim3  14534  isumadd  14542  fsump1i  14544  fsummulc2  14560  fsumrelem  14583  iserabs  14591  cvgcmp  14592  cvgcmpub  14593  cvgcmpce  14594  binom1dif  14609  isumshft  14615  isumsplit  14616  isumrpcl  14619  isumsup2  14622  climcndslem1  14625  climcndslem2  14626  climcnds  14627  arisum2  14637  trireciplem  14638  geoser  14643  geolim  14645  geo2lim  14650  cvgrat  14659  mertenslem1  14660  mertenslem2  14661  mertens  14662  clim2prod  14664  clim2div  14665  ntrivcvgfvn0  14675  ntrivcvgtail  14676  prodeq2ii  14687  prodmolem3  14707  prodmolem2a  14708  fprod  14715  fprodntriv  14716  fprodss  14722  fprodser  14723  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodabs  14748  fprodeq0  14749  fprodn0  14753  iprodclim3  14775  iprodmul  14778  fallfacfwd  14811  0fallfac  14812  binomfallfaclem2  14815  fallfacval4  14818  bpolysum  14828  bpolydiflem  14829  fsumkthpow  14831  efcvgfsum  14860  efcj  14866  fprodefsum  14869  effsumlt  14885  ruclem7  15009  bitsfzolem  15203  bitsfzo  15204  bitsfi  15206  bitsinv1lem  15210  bitsinv1  15211  bitsinvp1  15218  sadcp1  15224  sadadd  15236  sadass  15240  bitsres  15242  smupp1  15249  smuval2  15251  smupval  15257  smueqlem  15259  smumul  15262  algrp1  15334  phiprmpw  15528  crth  15530  phimullem  15531  eulerthlem2  15534  prmdiv  15537  pcpremul  15595  pcmpt  15643  pcfac  15650  pockthlem  15656  pockthg  15657  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  prmrec  15673  1arith  15678  vdwapun  15725  vdwlem1  15732  vdwlem2  15733  vdwlem3  15734  vdwlem6  15737  vdwlem8  15739  vdwlem10  15741  vdw  15745  imasvscafn  16244  xpsfrnel2  16272  oppccatid  16426  oppccomfpropd  16434  brcic  16505  funcoppc  16582  invfuc  16681  hofcl  16946  yonedalem4c  16964  gsumwsubmcl  17422  gsumccat  17425  gsumwmhm  17429  mulgnnp1  17596  mulgnnsubcl  17600  mulgnn0z  17614  mulgnndir  17616  mulgnndirOLD  17617  psgnunilem4  17963  psgnran  17981  sylow1lem1  18059  lsmmod2  18135  lsmdisj2r  18144  efginvrel2  18186  efgsdmi  18191  efgsrel  18193  efgs1b  18195  efgsp1  18196  efgredleme  18202  efgredlemc  18204  efgcpbllemb  18214  frgpuplem  18231  mulgnn0di  18277  frgpnabllem1  18322  lt6abl  18342  cycsubgcyg  18348  gsumval3eu  18351  gsumval3  18354  gsumzcl2  18357  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  gsumzoppg  18390  telgsumfz0s  18434  dprdwd  18456  dprd2da  18487  pgpfaclem1  18526  srgbinom  18591  isirred  18745  lspprid2  19046  lspsnat  19193  lsppratlem1  19195  lsppratlem3  19197  lidl0cl  19260  lidlacl  19261  lidlnegcl  19262  lidlmcl  19265  psrbaglefi  19420  psrass23l  19456  psrass23  19458  mplcoe5lem  19515  mpfind  19584  psr1bascl  19618  ply1basf  19620  gsummoncoe1  19722  lply1binom  19724  lply1binomsc  19725  mpfpf1  19763  pf1mpf  19764  evl1scvarpw  19775  psgnghm  19974  matbas2i  20276  matecld  20280  matgsum  20291  mpt2matmul  20300  dmatmul  20351  1mavmul  20402  mdetleib2  20442  m1detdiag  20451  marep01ma  20514  smadiadetlem4  20523  slesolinv  20534  pmatcollpw3fi1lem1  20639  chpscmat  20695  chpscmatgsumbin  20697  chp0mat  20699  chpidmat  20700  chfacfisf  20707  chfacfisfcpmat  20708  chfacfpmmulgsum2  20718  cldrcl  20878  ordtbas  21044  iscnp2  21091  dis1stc  21350  ptbasfi  21432  ptpjopn  21463  ptclsg  21466  ptcnp  21473  kqtop  21596  reghmph  21644  ptcmplem2  21904  ptcmplem3  21905  ptcmplem4  21906  tsmslem1  21979  utop2nei  22101  isucn2  22130  cuspcvg  22152  cnextucn  22154  imasdsf1olem  22225  blcvx  22648  xrhmeo  22792  cnrehmeo  22799  evth  22805  reparphti  22843  iscau4  23123  iscmet3lem1  23135  lmle  23145  rrxfsupp  23231  pjthlem2  23255  ovollb2lem  23302  ovolunlem1a  23310  ovoliunlem1  23316  ovoliun2  23320  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem4  23334  iundisj2  23363  voliunlem1  23364  volsup  23370  ioombl1lem4  23375  uniioovol  23393  uniioombllem3  23399  uniioombllem4  23400  uniioombllem6  23402  vitalilem5  23426  mbfimaopnlem  23467  mbflimsup  23478  mbfi1fseqlem3  23529  iblitg  23580  dvnp1  23733  cpncn  23744  dvlip2  23803  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumrlimge0  23838  dvfsumrlim2  23840  ftc1cn  23851  elplyd  24003  ply1termlem  24004  ply1term  24005  ply0  24009  plyeq0lem  24011  plyaddlem1  24014  plymullem1  24015  plyaddlem  24016  plymullem  24017  coeeulem  24025  plyco  24042  coeeq2  24043  coefv0  24049  coemulhi  24055  coemulc  24056  plycj  24078  dvply1  24084  vieta1lem2  24111  elqaalem2  24120  dvtaylp  24169  dvntaylp  24170  taylthlem1  24172  taylth  24174  ulmres  24187  ulmshftlem  24188  ulmshft  24189  ulmcau  24194  ulmdvlem1  24199  mtest  24203  mtestbdd  24204  pserulm  24221  psercn2  24222  psercnlem1  24224  psercn  24225  pserdvlem2  24227  abelthlem6  24235  abelth  24240  efif1olem1  24333  efif1olem3  24335  efif1olem4  24336  logcn  24438  advlogexp  24446  efopn  24449  cxpeq  24543  asinsin  24664  atantayl  24709  leibpilem2  24713  birthdaylem2  24724  birthdaylem3  24725  efrlim  24741  emcllem2  24768  emcllem5  24771  emcllem7  24773  harmonicbnd4  24782  fsumharmonic  24783  lgamgulm2  24807  lgamcvglem  24811  lgamcvg2  24826  gamcvg2lem  24830  wilthlem2  24840  wilthlem3  24841  ftalem1  24844  ftalem2  24845  ftalem3  24846  ftalem5  24848  basellem2  24853  basellem3  24854  basellem5  24856  basellem8  24859  ppiprm  24922  ppinprm  24923  chtprm  24924  chtnprm  24925  chpp1  24926  vma1  24937  ppiltx  24948  musum  24962  0sgmppw  24968  1sgmprm  24969  ppiublem2  24973  chtublem  24981  fsumvma2  24984  chpchtsum  24989  logexprlim  24995  bposlem5  25058  lgscllem  25074  lgsval2lem  25077  lgsval4a  25089  lgsneg  25091  lgsdir2lem3  25097  lgsdir2lem5  25099  lgsdir  25102  lgsdilem2  25103  lgsdi  25104  lgsne0  25105  gausslemma2dlem3  25138  lgseisenlem1  25145  lgsquadlem2  25151  chebbnd1lem1  25203  chtppilimlem1  25207  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrmusum2  25228  dchrvmasum2lem  25230  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0flb  25244  dchrisum0re  25247  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  mudivsum  25264  mulogsum  25266  mulog2sumlem2  25269  selberg2lem  25284  logdivbnd  25290  pntrsumo1  25299  pntrsumbnd2  25301  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntrlog2bndlem6a  25316  pntlemj  25337  pntlemf  25339  ostth2lem3  25369  tglngne  25490  ltgseg  25536  eedimeq  25823  axlowdimlem16  25882  ebtwntg  25907  subgruhgredgd  26221  subumgredg2  26222  umgrres1lem  26247  wlkson  26608  wksonproplem  26657  trlsonfval  26658  pthsonfval  26692  spthson  26693  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  eupth2lems  27216  numclwlk1lem2foa  27344  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  htthlem  27902  hhsscms  28264  shmodsi  28376  pjoc1i  28418  5oalem1  28641  mayete3i  28715  adj1  28920  iundisj2f  29529  fmptco1f1o  29562  fcnvgreu  29600  ssnnssfz  29677  iundisj2fi  29684  pmtrto1cl  29977  psgnfzto1stlem  29978  fzto1st1  29980  1smat1  29998  submateqlem2  30002  lmatfval  30008  mdetlap1  30020  madjusmdetlem1  30021  madjusmdetlem2  30022  madjusmdetlem3  30023  madjusmdetlem4  30024  pnfneige0  30125  pl1cn  30129  rrhqima  30186  indpreima  30215  esumfzf  30259  esumpcvgval  30268  esumpmono  30269  esumcvg  30276  ldgenpisyslem1  30354  ldgenpisys  30357  measbase  30388  dya2iocnei  30472  oddpwdc  30544  eulerpartlems  30550  eulerpartlemb  30558  sseqf  30582  fibp1  30591  orrvcval4  30654  orrvcoel  30655  orrvccel  30656  ballotlem2  30678  ballotlemfrceq  30718  signsplypnf  30755  signswch  30766  signstf0  30773  signstfvn  30774  signstfvneq0  30777  signstfvcl  30778  signstfveq0  30782  signsvfn  30787  fct2relem  30803  fsum2dsub  30813  reprsuc  30821  reprpmtf1o  30832  breprexplema  30836  breprexplemc  30838  hgt749d  30855  hgt750lemb  30862  tgoldbachgnn  30865  bnj1172  31195  bnj1245  31208  bnj1311  31218  bnj1450  31244  bnj1501  31261  subfacp1lem1  31287  subfacp1lem5  31292  subfacp1lem6  31293  subfacval2  31295  erdszelem7  31305  cvxsconn  31351  cvmliftlem5  31397  cvmliftlem7  31399  cvmliftlem10  31402  cvmliftlem13  31404  mrsubvrs  31545  msubrn  31552  msubco  31554  msubvrs  31583  imageval  32162  fwddifnp1  32397  knoppcnlem8  32615  knoppcnlem10  32617  icoreunrn  33337  istoprelowl  33338  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  mblfinlem2  33577  ftc1cnnc  33614  upixp  33654  sdclem2  33668  caushft  33687  ismtyres  33737  rrnmet  33758  rrndstprj1  33759  rrndstprj2  33760  rrncmslem  33761  rrnequiv  33764  iccbnd  33769  osumcllem7N  35566  pexmidlem4N  35577  lcfrlem4  37151  lcfrlem5  37152  lcfrlem6  37153  lcfrlem16  37164  lcfrlem38  37186  mapdrvallem2  37251  mapdh8ab  37383  mapdh8ad  37385  mapdh8e  37390  mapfzcons  37596  diophren  37694  irrapxlem1  37703  monotuz  37823  acongeq  37867  jm2.26lem3  37885  jm3.1lem2  37902  pw2f1ocnv  37921  idomodle  38091  trclfvdecomr  38337  imo72b2lem1  38788  dvgrat  38828  cvgdvgrat  38829  hashnzfz2  38837  fcnre  39498  refsumcn  39503  rfcnnnub  39509  disjf1o  39692  disjinfi  39694  ssmapsn  39722  ssuzfz  39878  nnsplit  39887  uzssd2  39957  uzublem  39970  fsumsermpt  40129  climsuselem1  40157  limcperiod  40178  sumnnodd  40180  lptioo2cn  40195  lptioo1cn  40196  climresmpt  40209  allbutfifvre  40225  climleltrp  40226  cnrefiisplem  40373  cncfshift  40405  cncfperiod  40410  cncfshiftioo  40423  fperdvper  40451  dvnmptdivc  40471  dvnmul  40476  dvmptfprod  40478  dvnprodlem3  40481  stoweidlem11  40546  stoweidlem15  40550  stoweidlem17  40552  stoweidlem20  40555  stoweidlem34  40569  stoweidlem35  40570  stoweidlem46  40581  stoweidlem47  40582  stoweidlem56  40591  stoweidlem59  40594  stoweidlem62  40597  stirlinglem5  40613  stirlinglem14  40622  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  fourierdlem11  40653  fourierdlem15  40657  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem25  40667  fourierdlem48  40689  fourierdlem52  40693  fourierdlem54  40695  fourierdlem58  40699  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem69  40710  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem80  40721  fourierdlem81  40722  fourierdlem83  40724  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  fouriercnp  40761  fouriersw  40766  elaa2lem  40768  etransclem4  40773  etransclem7  40776  etransclem10  40779  etransclem14  40783  etransclem15  40784  etransclem24  40793  etransclem25  40794  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem44  40813  etransclem46  40815  qndenserrnopnlem  40835  qndenserrn  40837  prsal  40856  salgencntex  40879  subsaliuncl  40894  subsalsal  40895  sge0tsms  40915  sge0fodjrnlem  40951  sge0isum  40962  iundjiunlem  40994  iundjiun  40995  meadjiunlem  41000  meaiunlelem  41003  meaiuninclem  41015  meaiininc2  41023  caragensplit  41035  carageneld  41037  carageniuncllem1  41056  caratheodorylem1  41061  caratheodorylem2  41062  hoicvr  41083  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem2  41131  hoiqssbllem2  41158  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  smflimlem3  41302  smfmullem4  41322  smfsupxr  41343  smflimsuplem2  41348  smflimsuplem5  41351  elmod2  41665  pwdif  41826  ssnn0ssfz  42452  zlmodzxzscm  42460  rmsupp0  42474  lincsum  42543  lincscm  42544  lindslinindimp2lem4  42575  lincresunit3  42595  elbigofrcl  42669  setrec1  42763  aacllem  42875
  Copyright terms: Public domain W3C validator