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

Theorem syl6eleq 2698
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 2690 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  syl6eleqr  2699  3eltr3g  2704  prid2g  4240  ndmfvrcl  6114  fnwelem  7157  tz7.48-1  7403  brwitnlem  7452  oeeulem  7546  dffi3  8198  cnfcom3lem  8461  alephgeom  8766  fpwwe2lem6  9314  canthwelem  9329  hargch  9352  r1wunlim  9416  eluzel2  11527  fseq1p1m1  12241  fznn0sub2  12273  nn0split  12281  fz1fzo0m1  12341  exple1  12740  digit1  12818  bcval5  12925  bcpasc  12928  hashf1  13053  seqcoll  13060  seqcoll2  13061  ccatrn  13174  swrdccat1  13258  swrdccat2  13259  cats1un  13276  splfv2a  13307  splval2  13308  caubnd  13895  limsupgre  14009  clim2ser  14182  clim2ser2  14183  iserex  14184  isermulc2  14185  iserle  14187  iserge0  14188  climub  14189  climserle  14190  isercolllem2  14193  isercolllem3  14194  isercoll  14195  isercoll2  14196  serf0  14208  iseraltlem2  14210  iseraltlem3  14211  iseralt  14212  sumeq2ii  14220  summolem3  14241  summolem2a  14242  fsum  14247  sum0  14248  fsumcl2lem  14258  fsumadd  14266  isumclim3  14281  isumadd  14289  fsump1i  14291  fsummulc2  14307  fsumrelem  14329  iserabs  14337  cvgcmp  14338  cvgcmpub  14339  cvgcmpce  14340  binom1dif  14353  isumshft  14359  isumsplit  14360  isumrpcl  14363  isumsup2  14366  climcndslem1  14369  climcndslem2  14370  climcnds  14371  arisum2  14381  trireciplem  14382  geoser  14387  geolim  14389  geo2lim  14394  cvgrat  14403  mertenslem1  14404  mertenslem2  14405  mertens  14406  clim2prod  14408  clim2div  14409  ntrivcvgfvn0  14419  ntrivcvgtail  14420  prodeq2ii  14431  prodmolem3  14451  prodmolem2a  14452  fprod  14459  fprodntriv  14460  fprodss  14466  fprodser  14467  fprodcl2lem  14468  fprodmul  14478  fproddiv  14479  fprodabs  14492  fprodeq0  14493  fprodn0  14497  iprodclim3  14519  iprodmul  14522  fallfacfwd  14555  0fallfac  14556  binomfallfaclem2  14559  fallfacval4  14562  bpolysum  14572  bpolydiflem  14573  fsumkthpow  14575  efcvgfsum  14604  efcj  14610  fprodefsum  14613  effsumlt  14629  ruclem7  14753  bitsfzolem  14943  bitsfzo  14944  bitsfi  14946  bitsinv1lem  14950  bitsinv1  14951  bitsinvp1  14958  sadcp1  14964  sadadd  14976  sadass  14980  bitsres  14982  smupp1  14989  smuval2  14991  smupval  14997  smueqlem  14999  smumul  15002  algrp1  15074  phiprmpw  15268  crth  15270  phimullem  15271  eulerthlem2  15274  prmdiv  15277  pcpremul  15335  pcmpt  15383  pcfac  15390  pockthlem  15396  pockthg  15397  prmreclem2  15408  prmreclem3  15409  prmreclem4  15410  prmreclem5  15411  prmreclem6  15412  prmrec  15413  1arith  15418  vdwapun  15465  vdwlem1  15472  vdwlem2  15473  vdwlem3  15474  vdwlem6  15477  vdwlem8  15479  vdwlem10  15481  vdw  15485  imasvscafn  15969  xpsfrnel2  15997  oppccatid  16151  oppccomfpropd  16159  brcic  16230  funcoppc  16307  invfuc  16406  hofcl  16671  yonedalem4c  16689  gsumwsubmcl  17147  gsumccat  17150  gsumwmhm  17154  mulgnnp1  17321  mulgnnsubcl  17325  mulgnn0z  17339  mulgnndir  17341  mulgnndirOLD  17342  psgnunilem4  17689  psgnran  17707  sylow1lem1  17785  lsmmod2  17861  lsmdisj2r  17870  efginvrel2  17912  efgsdmi  17917  efgsrel  17919  efgs1b  17921  efgsp1  17922  efgredleme  17928  efgredlemc  17930  efgcpbllemb  17940  frgpuplem  17957  mulgnn0di  18003  frgpnabllem1  18048  lt6abl  18068  cycsubgcyg  18074  gsumval3eu  18077  gsumval3  18080  gsumzcl2  18083  gsumzaddlem  18093  gsumconst  18106  gsumzmhm  18109  gsumzoppg  18116  telgsumfz0s  18160  dprdwd  18182  dprd2da  18213  pgpfaclem1  18252  srgbinom  18317  isirred  18471  lspprid2  18768  lspsnat  18915  lsppratlem1  18917  lsppratlem3  18919  lidl0cl  18982  lidlacl  18983  lidlnegcl  18984  lidlmcl  18987  psrbaglefi  19142  psrass23l  19178  psrass23  19180  mplcoe5lem  19237  mpfind  19306  psr1bascl  19340  ply1basf  19342  gsummoncoe1  19444  lply1binom  19446  lply1binomsc  19447  mpfpf1  19485  pf1mpf  19486  evl1scvarpw  19497  psgnghm  19693  matbas2i  19995  matecld  19999  matgsum  20010  mpt2matmul  20019  dmatmul  20070  1mavmul  20121  mdetleib2  20161  m1detdiag  20170  marep01ma  20233  smadiadetlem4  20242  slesolinv  20253  pmatcollpw3fi1lem1  20358  chpscmat  20414  chpscmatgsumbin  20416  chp0mat  20418  chpidmat  20419  chfacfisf  20426  chfacfisfcpmat  20427  chfacfpmmulgsum2  20437  cldrcl  20588  ordtbas  20754  iscnp2  20801  dis1stc  21060  ptbasfi  21142  ptpjopn  21173  ptclsg  21176  ptcnp  21183  kqtop  21306  reghmph  21354  ptcmplem2  21615  ptcmplem3  21616  ptcmplem4  21617  tsmslem1  21690  utop2nei  21812  isucn2  21841  cuspcvg  21863  cnextucn  21865  imasdsf1olem  21936  blcvx  22357  xrhmeo  22501  cnrehmeo  22508  evth  22514  reparphti  22553  iscau4  22830  iscmet3lem1  22842  lmle  22852  rrxfsupp  22938  pjthlem2  22962  ovollb2lem  23008  ovolunlem1a  23016  ovoliunlem1  23022  ovoliun2  23026  ovolscalem1  23033  ovolicc1  23036  ovolicc2lem4  23040  iundisj2  23069  voliunlem1  23070  volsup  23076  ioombl1lem4  23081  uniioovol  23098  uniioombllem3  23104  uniioombllem4  23105  uniioombllem6  23107  vitalilem5  23132  mbfimaopnlem  23173  mbflimsup  23184  mbfi1fseqlem3  23235  iblitg  23286  dvnp1  23439  cpncn  23450  dvlip2  23507  dvfsumlem2  23539  dvfsumlem3  23540  dvfsumrlimge0  23542  dvfsumrlim2  23544  ftc1cn  23555  elplyd  23707  ply1termlem  23708  ply1term  23709  ply0  23713  plyeq0lem  23715  plyaddlem1  23718  plymullem1  23719  plyaddlem  23720  plymullem  23721  coeeulem  23729  plyco  23746  coeeq2  23747  coefv0  23753  coemulhi  23759  coemulc  23760  plycj  23782  dvply1  23788  vieta1lem2  23815  elqaalem2  23824  dvtaylp  23873  dvntaylp  23874  taylthlem1  23876  taylth  23878  ulmres  23891  ulmshftlem  23892  ulmshft  23893  ulmcau  23898  ulmdvlem1  23903  mtest  23907  mtestbdd  23908  pserulm  23925  psercn2  23926  psercnlem1  23928  psercn  23929  pserdvlem2  23931  abelthlem6  23939  abelth  23944  efif1olem1  24037  efif1olem3  24039  efif1olem4  24040  logcn  24138  advlogexp  24146  efopn  24149  cxpeq  24243  asinsin  24364  atantayl  24409  leibpilem2  24413  birthdaylem2  24424  birthdaylem3  24425  efrlim  24441  emcllem2  24468  emcllem5  24471  emcllem7  24473  harmonicbnd4  24482  fsumharmonic  24483  lgamgulm2  24507  lgamcvglem  24511  lgamcvg2  24526  gamcvg2lem  24530  wilthlem2  24540  wilthlem3  24541  ftalem1  24544  ftalem2  24545  ftalem3  24546  ftalem5  24548  basellem2  24553  basellem3  24554  basellem5  24556  basellem8  24559  ppiprm  24622  ppinprm  24623  chtprm  24624  chtnprm  24625  chpp1  24626  vma1  24637  ppiltx  24648  musum  24662  0sgmppw  24668  1sgmprm  24669  ppiublem2  24673  chtublem  24681  fsumvma2  24684  chpchtsum  24689  logexprlim  24695  bposlem5  24758  lgscllem  24774  lgsval2lem  24777  lgsval4a  24789  lgsneg  24791  lgsdir2lem3  24797  lgsdir2lem5  24799  lgsdir  24802  lgsdilem2  24803  lgsdi  24804  lgsne0  24805  gausslemma2dlem3  24838  lgseisenlem1  24845  lgsquadlem2  24851  chebbnd1lem1  24903  chtppilimlem1  24907  rplogsumlem2  24919  rpvmasumlem  24921  dchrisumlem1  24923  dchrisumlem2  24924  dchrmusum2  24928  dchrvmasum2lem  24930  dchrvmasumiflem1  24935  dchrisum0flblem1  24942  dchrisum0flblem2  24943  dchrisum0flb  24944  dchrisum0re  24947  dchrisum0lem1b  24949  dchrisum0lem1  24950  dchrisum0lem2a  24951  dchrisum0lem2  24952  dchrisum0lem3  24953  mudivsum  24964  mulogsum  24966  mulog2sumlem2  24969  selberg2lem  24984  logdivbnd  24990  pntrsumo1  24999  pntrsumbnd2  25001  pntrlog2bndlem2  25012  pntrlog2bndlem4  25014  pntrlog2bndlem6a  25016  pntlemj  25037  pntlemf  25039  ostth2lem3  25069  tglngne  25191  ltgseg  25237  eedimeq  25524  axlowdimlem16  25583  ebtwntg  25608  eupares  26296  eupap1  26297  eupath2lem3  26300  eupath2  26301  htthlem  26952  hhsscms  27314  shmodsi  27426  pjoc1i  27468  5oalem1  27691  mayete3i  27765  adj1  27970  iundisj2f  28579  fcnvgreu  28649  ssnnssfz  28731  iundisj2fi  28737  pmtrto1cl  28974  psgnfzto1stlem  28975  fzto1st1  28977  1smat1  28992  submateqlem2  28996  lmatfval  29002  mdetlap1  29014  madjusmdetlem1  29015  madjusmdetlem2  29016  madjusmdetlem3  29017  madjusmdetlem4  29018  pnfneige0  29119  pl1cn  29123  rrhqima  29180  indpreima  29208  esumfzf  29252  esumpcvgval  29261  esumpmono  29262  esumcvg  29269  ldgenpisyslem1  29347  ldgenpisys  29350  measbase  29381  dya2iocnei  29465  oddpwdc  29537  eulerpartlems  29543  eulerpartlemb  29551  sseqf  29575  fibp1  29584  orrvcval4  29647  orrvcoel  29648  orrvccel  29649  ballotlem2  29671  ballotlemfrceq  29711  signsplypnf  29747  signswch  29758  signstf0  29765  signstfvn  29766  signstfvneq0  29769  signstfvcl  29770  signstfveq0  29774  signsvfn  29779  bnj1172  30117  bnj1245  30130  bnj1311  30140  bnj1450  30166  bnj1501  30183  subfacp1lem1  30209  subfacp1lem5  30214  subfacp1lem6  30215  subfacval2  30217  erdszelem7  30227  cvxscon  30273  cvmliftlem5  30319  cvmliftlem7  30321  cvmliftlem10  30324  cvmliftlem13  30326  mrsubvrs  30467  msubrn  30474  msubco  30476  msubvrs  30505  bdayelon  30873  imageval  31001  fwddifnp1  31236  knoppcnlem8  31454  knoppcnlem10  31456  icoreunrn  32177  istoprelowl  32178  poimirlem3  32376  poimirlem4  32377  poimirlem6  32379  poimirlem7  32380  poimirlem8  32381  poimirlem12  32385  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem18  32391  poimirlem19  32392  poimirlem20  32393  poimirlem21  32394  poimirlem22  32395  poimirlem23  32396  poimirlem24  32397  poimirlem25  32398  poimirlem26  32399  poimirlem27  32400  poimirlem28  32401  poimirlem29  32402  poimirlem31  32404  mblfinlem2  32411  ftc1cnnc  32448  upixp  32488  sdclem2  32502  caushft  32521  ismtyres  32571  rrnmet  32592  rrndstprj1  32593  rrndstprj2  32594  rrncmslem  32595  rrnequiv  32598  iccbnd  32603  osumcllem7N  34060  pexmidlem4N  34071  lcfrlem4  35646  lcfrlem5  35647  lcfrlem6  35648  lcfrlem16  35659  lcfrlem38  35681  mapdrvallem2  35746  mapdh8ab  35878  mapdh8ad  35880  mapdh8e  35885  mapfzcons  36091  diophren  36189  irrapxlem1  36198  monotuz  36318  acongeq  36362  jm2.26lem3  36380  jm3.1lem2  36397  pw2f1ocnv  36416  idomodle  36587  trclfvdecomr  36833  imo72b2lem1  37287  dvgrat  37327  cvgdvgrat  37328  hashnzfz2  37336  fcnre  38001  refsumcn  38006  rfcnnnub  38012  disjf1o  38167  disjinfi  38169  ssmapsn  38197  ssuzfz  38300  nnsplit  38309  fsumsermpt  38440  climsuselem1  38468  limcperiod  38489  sumnnodd  38491  lptioo2cn  38506  lptioo1cn  38507  climresmpt  38520  allbutfifvre  38536  climleltrp  38537  cncfshift  38553  cncfperiod  38558  cncfshiftioo  38572  fperdvper  38602  dvnmptdivc  38622  dvnmul  38627  dvmptfprod  38629  dvnprodlem3  38632  stoweidlem11  38698  stoweidlem15  38702  stoweidlem17  38704  stoweidlem20  38707  stoweidlem34  38721  stoweidlem35  38722  stoweidlem46  38733  stoweidlem47  38734  stoweidlem56  38743  stoweidlem59  38746  stoweidlem62  38749  stirlinglem5  38765  stirlinglem14  38774  dirkertrigeqlem2  38786  dirkertrigeqlem3  38787  fourierdlem11  38805  fourierdlem15  38809  fourierdlem16  38810  fourierdlem21  38815  fourierdlem22  38816  fourierdlem25  38819  fourierdlem48  38841  fourierdlem52  38845  fourierdlem54  38847  fourierdlem58  38851  fourierdlem62  38855  fourierdlem64  38857  fourierdlem65  38858  fourierdlem69  38862  fourierdlem70  38863  fourierdlem71  38864  fourierdlem73  38866  fourierdlem80  38873  fourierdlem81  38874  fourierdlem83  38876  fourierdlem92  38885  fourierdlem93  38886  fourierdlem97  38890  fourierdlem103  38896  fourierdlem104  38897  fourierdlem112  38905  fourierdlem113  38906  fouriercnp  38913  fouriersw  38918  elaa2lem  38920  etransclem4  38925  etransclem7  38928  etransclem10  38931  etransclem14  38935  etransclem15  38936  etransclem24  38945  etransclem25  38946  etransclem31  38952  etransclem32  38953  etransclem35  38956  etransclem44  38965  etransclem46  38967  qndenserrnopnlem  38987  qndenserrn  38989  prsal  39008  salgencntex  39031  subsaliuncl  39046  subsalsal  39047  sge0tsms  39067  sge0fodjrnlem  39103  sge0isum  39114  iundjiunlem  39146  iundjiun  39147  meadjiunlem  39152  meaiunlelem  39155  meaiuninclem  39167  meaiininc2  39172  caragensplit  39184  carageneld  39186  carageniuncllem1  39205  caratheodorylem1  39210  caratheodorylem2  39211  hoicvr  39232  hsphoidmvle2  39269  hsphoidmvle  39270  hoidmv1lelem2  39276  hoidmv1lelem3  39277  hoidmvlelem2  39280  hoiqssbllem2  39307  pimdecfgtioc  39396  pimincfltioc  39397  pimdecfgtioo  39398  pimincfltioo  39399  smflimlem3  39453  smfmullem4  39473  elmod2  39745  pwdif  39834  subgruhgredgd  40500  subumgredg2  40501  umgrres1lem  40521  wlkson  40856  1wlksonproplem  40904  trlsonfval  40905  pthsonfval  40938  spthson  40939  crctcsh1wlkn0lem4  41008  crctcsh1wlkn0lem5  41009  eupth2lems  41398  ssnn0ssfz  41912  zlmodzxzscm  41920  rmsupp0  41935  lincsum  42004  lincscm  42005  lindslinindimp2lem4  42036  lincresunit3  42056  elbigofrcl  42134  aacllem  42309
  Copyright terms: Public domain W3C validator