Theorem mp1i 13

Description: Inference detaching an antecedent and introducing a new one. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.1	⊢ 𝜑
mp1i.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mp1i	⊢ (𝜒 → 𝜓)

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.1	. . 3 ⊢ 𝜑
2		mp1i.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4	3	a1i 11	1 ⊢ (𝜒 → 𝜓)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  sbcg  3863  relsnopg  5813  poirr2  6144  fvrnressn  7181  isomin  7357  isoini  7358  mptmpoopabbrdOLDOLD  8108  opco1  8148  opco2  8149  supp0  8190  suppval1  8191  suppssr  8220  dmtpos  8263  mpocurryd  8294  oaabs2  8687  elqsecl  8811  mapsncnv  8933  boxcutc  8981  domunsncan  9112  findcard2d  9206  unxpdom2  9290  sucxpdom  9291  ac6sfi  9320  imafi  9353  xpfiOLD  9359  snopfsupp  9431  fifo  9472  ordtypelem4  9561  oismo  9580  wofib  9585  brwdom2  9613  canthwdom  9619  cantnfval  9708  cantnflt  9712  cantnff  9714  cantnf0  9715  cantnflem1b  9726  cantnflem1  9729  cnfcom  9740  cnfcom2lem  9741  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  ranksnb  9867  updjudhcoinlf  9972  updjudhcoinrg  9973  updjud  9974  tskwe  9990  cardidm  9999  infxpenc  10058  fseqdom  10066  dfac8clem  10072  dfac12lem2  10185  infmap2  10257  fin23lem14  10373  fin23lem40  10391  isf34lem7  10419  isf34lem6  10420  fin1a2lem12  10451  hsmexlem4  10469  hsmexlem5  10470  ac5b  10518  alephexp1  10619  alephsuc3  10620  fpwwe2lem7  10677  fpwwe2lem12  10682  canthwe  10691  canthp1lem2  10693  gchdju1  10696  pwfseqlem5  10703  wunco  10773  prlem934  11073  supsrlem  11151  msqge0  11784  negfi  12217  ofnegsub  12264  ofsubge0  12265  xaddpnf1  13268  supxrmnf  13359  fz0sn0fz1  13685  injresinjlem  13826  fldiv4lem1div2  13877  uzindi  14023  seqfeq4  14092  seqof  14100  bcval5  14357  hashdomi  14419  hash1snb  14458  hashmap  14474  hashge2el2difr  14520  hashtpg  14524  fi1uzind  14546  ccatlen  14613  ccat0  14614  lswccatn0lsw  14629  ccatalpha  14631  s111  14653  ccat2s1fvw  14676  swrd0  14696  swrdwrdsymb  14700  swrdspsleq  14703  reps  14808  repsw0  14815  repswccat  14824  repswrevw  14825  lswcshw  14853  cshwsexaOLD  14863  scshwfzeqfzo  14865  lsws2  14943  lsws3  14944  lsws4  14945  wrdlen2i  14981  s2rn  15002  s3rn  15003  s7rn  15004  relexpsucnnr  15064  relexpaddg  15092  shftfib  15111  reusq0  15501  limsupcl  15509  limsupgf  15511  limsupval2  15516  isercolllem3  15703  modfsummods  15829  ackbijnn  15864  supcvg  15892  fprodfac  16009  fprodmodd  16033  fallfac0  16064  bpoly4  16095  ege2le3  16126  rpnnen2lem5  16254  ruclem11  16276  fsumdvds  16345  fproddvdsd  16372  mod2eq1n2dvds  16384  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  bitsinv2  16480  sadaddlem  16503  smupf  16515  smup0  16516  smu01lem  16522  nn0rppwr  16598  3lcm2e6woprm  16652  6lcm4e12  16653  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  coprmprod  16698  ge2nprmge4  16738  isprm6  16751  hashdvds  16812  phisum  16828  reumodprminv  16842  prmreclem6  16959  vdwlem13  17031  ramtlecl  17038  0ram  17058  prmdvdsprmo  17080  fvprmselgcd1  17083  prmgaplcmlem1  17089  prmgaplem7  17095  prmgaplcm  17098  cshwshashnsame  17141  prmlem0  17143  wunndx  17232  prdsval  17500  xpsbas  17617  xpsadd  17619  xpsmul  17620  xpssca  17621  xpsvsca  17622  xpsless  17623  xpsle  17624  mreexexlem2d  17688  mreacs  17701  acsfn  17702  isofn  17819  cicsym  17848  cicer  17850  idfu2nd  17922  idfucl  17926  fucsect  18020  initoeu2lem1  18059  initoeu2lem2  18060  setccatid  18129  setcepi  18133  catchomfval  18147  estrccatid  18176  estrreslem1  18181  estrreslem1OLD  18182  estrreslem2  18183  estrres  18184  funcestrcsetclem8  18192  fullestrcsetc  18196  embedsetcestrclem  18202  funcsetcestrclem8  18207  uncfval  18279  odulub  18452  odujoin  18453  oduglb  18454  odumeet  18455  isipodrs  18582  fpwipodrs  18585  isacs5lem  18590  idmgmhm  18714  idmhm  18808  submacs  18840  frmdup1  18877  efmndbas  18884  sursubmefmnd  18909  injsubmefmnd  18910  idresefmnd  18912  smndex1id  18924  mgmnsgrpex  18944  mulgneg2  19126  subgacs  19179  nsgacs  19180  1nsgtrivd  19192  idrespermg  19429  psgnunilem5  19512  psgnsn  19538  odf1o2  19591  frgpuplem  19790  cntrcmnd  19860  cygctb  19910  gsumpr  19973  gsumzunsnd  19974  gsum2dlem2  19989  gsummptnn0fz  20004  dprdsubg  20044  dmdprdsplit2lem  20065  dmdprdpr  20069  dprdpr  20070  dpjeq  20079  ablfac1eulem  20092  pgpfac1lem2  20095  pgpfaclem1  20101  prmgrpsimpgd  20134  ablsimpgprmd  20135  srgbinomlem4  20226  unitgrp  20383  isirred  20419  isrnghm  20441  brric  20504  isnzr2hash  20519  0ringnnzr  20525  0ring01eqbi  20532  dfrngc2  20628  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetcALT  20641  dfringc2  20657  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  rngcresringcat  20669  srhmsubc  20680  rngcrescrhm  20684  rhmsubclem3  20687  rng1nnzr  20776  fldc  20785  imadrhmcl  20798  subrgacs  20801  sdrgacs  20802  cntzsdrg  20803  mptscmfsupp0  20925  lssacs  20965  pwssplit1  21058  lbsextlem2  21161  lbsextlem3  21162  rlmlsm  21212  rnglidlmmgm  21255  xrsmcmn  21404  xrs1mnd  21422  xrs10  21423  gsumfsum  21452  zringlpir  21478  zringcyg  21480  pzriprnglem4  21495  zndvds  21568  regsumsupp  21640  frlmip  21798  uvcvv1  21809  lsslinds  21851  psrass1lem  21952  psrlidm  21982  resspsradd  21995  resspsrmul  21996  resspsrvsca  21997  mplcoe5lem  22057  ltbwe  22062  selvfval  22138  mhpvarcl  22152  psdmul  22170  coe1fsupp  22216  psropprmul  22239  coe1add  22267  coe1mul2lem1  22270  coe1tm  22276  cply1coe0bi  22306  evls1rhmlem  22325  evl1sca  22338  evl1var  22340  pf1mpf  22356  pf1ind  22359  evls1vsca  22377  evls1maplmhm  22381  matmulr  22444  ofco2  22457  mat0dimbas0  22472  mat1dimelbas  22477  mat1f1o  22484  dmatval  22498  scmatghm  22539  mavmul0  22558  mavmul0g  22559  m1detdiag  22603  mdetunilem9  22626  maducoeval2  22646  madugsum  22649  smadiadetlem0  22667  smadiadetlem1a  22669  smadiadetlem4  22675  smadiadetglem1  22677  smadiadetglem2  22678  smadiadetg  22679  cramer0  22696  cpmat  22715  mat2pmatfval  22729  cpm2mfval  22755  m2cpminvid2lem  22760  pmatcollpw3fi1lem2  22793  pmatcollpw3fi1  22794  idpm2idmp  22807  pm2mpmhmlem2  22825  chpmatfval  22836  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  cpmidpmatlem2  22877  cpmadugsumlemF  22882  cpmidgsum2  22885  cpmadumatpolylem1  22887  cayhamlem3  22893  cayhamlem4  22894  indistopon  23008  mreclatdemoBAD  23104  mnfnei  23229  resthauslem  23371  sshauslem  23380  discmp  23406  connima  23433  1stcfb  23453  ptbasfi  23589  hauseqlcld  23654  xkoptsub  23662  xkofvcn  23692  idqtop  23714  tgqtop  23720  kqdisj  23740  xpstopnlem1  23817  xpstopnlem2  23819  ufildom1  23934  alexsubb  24054  alexsubALTlem3  24057  ptcmplem2  24061  ptcmplem3  24062  tmdgsum  24103  ustneism  24232  ustuqtop1  24250  iducn  24292  prdsmet  24380  imasdsf1olem  24383  xpsxmet  24390  xpsdsval  24391  xpsmet  24392  prdsbl  24504  met1stc  24534  prdsxmslem2  24542  xpsxms  24547  xpsms  24548  psmetutop  24580  dscmet  24585  nmoffn  24732  nmofval  24735  nmolb  24738  nmof  24740  cnbl0  24794  xrsmopn  24834  xrge0gsumle  24855  xrge0tsms  24856  negfcncf  24950  cnrehmeo  24984  cnrehmeoOLD  24985  lebnum  24996  xlebnum  24997  reparphti  25029  reparphtiOLD  25030  pcopt  25055  pcopt2  25056  pcorevcl  25058  pcorevlem  25059  pi1xfrval  25087  pi1xfrcnvlem  25089  pi1xfrcnv  25090  pi1cof  25092  pi1coval  25093  nmhmcn  25153  cphsubrglem  25211  csscld  25283  cmetcaulem  25322  cmpcmet  25353  csschl  25410  rrxplusgvscavalb  25429  rrxsca  25430  ehleudis  25452  divcncf  25482  ovolunlem1  25532  ovolicc2lem4  25555  ioovolcl  25605  ioorcl2  25607  uniioovol  25614  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  dyadmbllem  25634  mbfsub  25697  itg1climres  25749  xrge0f  25766  itg2ge0  25770  itg20  25772  itg2monolem1  25785  itg2i1fseq2  25791  ibl0  25822  ellimc2  25912  limcflf  25916  dvreslem  25944  dvidlem  25950  dvmptresicc  25951  dvid  25953  cpnres  25973  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvfre  25989  dvexp  25991  dvrec  25993  dvmptid  25995  dvmptc  25996  dvmptntr  26009  dvexp3  26016  dvlipcn  26033  dveq0  26039  dv11cn  26040  lhop2  26054  ftc1a  26078  itgpowd  26091  tdeglem1  26097  tdeglem3  26098  tdeglem4  26099  tdeglem2  26100  mdeglt  26104  mdegxrcl  26106  mdegcl  26108  mdeg0  26109  mdegle0  26116  ply1remlem  26204  plypf1  26251  coe0  26295  dvply1  26325  elqaalem3  26363  aaliou2b  26383  aaliou3lem8  26387  aaliou3lem7  26391  taylfvallem  26399  taylf  26402  tayl0  26403  taylpfval  26406  taylply  26411  dvtaylp  26412  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem1  26443  ulmdvlem2  26444  ulmdvlem3  26445  radcnvcl  26460  psercnlem2  26468  psercn  26470  pserdv  26473  abelthlem3  26477  abelth  26485  sincn  26488  coscn  26489  reefgim  26494  tangtx  26547  pige3ALT  26562  cos02pilt1  26568  cosordlem  26572  logcn  26689  dvlog  26693  advlog  26696  advlogexp  26697  logtayl  26702  logccv  26705  dvcxp1  26782  dvcncxp1  26785  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  sqrtcn  26793  loglesqrt  26804  logbfval  26833  isosctrlem2  26862  dquartlem1  26894  quart  26904  atancj  26953  efiatan  26955  atantan  26966  atanbndlem  26968  atansopn  26975  dvatan  26978  atantayl  26980  leibpilem2  26984  leibpi  26985  log2tlbnd  26988  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  divsqrtsumlem  27023  jensenlem1  27030  jensenlem2  27031  jensen  27032  amgmlem  27033  amgm  27034  emcllem4  27042  emcllem7  27045  lgamcvg2  27098  gamcvg2lem  27102  wilthlem2  27112  wilthlem3  27113  basellem6  27129  chtrpcl  27218  ppiltx  27220  1sgm2ppw  27244  chtlepsi  27250  chpub  27264  logfacbnd3  27267  logfacrlim  27268  perfectlem2  27274  dchrelbas2  27281  dchrabs  27304  dchrhash  27315  bposlem7  27334  lgsdir2lem5  27373  lgsqrlem1  27390  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgseisenlem4  27422  lgsquad2lem1  27428  lgsquad3  27431  2sqreu  27500  2sqreunn  27501  2sqreult  27502  2sqreultb  27503  2sqreunnlt  27504  chpo1ub  27524  vmadivsumb  27527  rpvmasumlem  27531  dchrisumlem2  27534  dchrmusumlema  27537  dchrvmasumlem2  27542  dchrvmasumlema  27544  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0lem1  27560  rplogsum  27571  mudivsum  27574  logdivsum  27577  mulog2sumlem2  27579  vmalogdivsum2  27582  2vmadivsumlem  27584  log2sumbnd  27588  selberglem2  27590  selbergb  27593  selberg2lem  27594  selberg2b  27596  selberg3lem1  27601  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntibndlem1  27633  pntibndlem2  27635  pntibndlem3  27636  pntlemb  27641  pntlemr  27646  pntlemf  27649  pntlem3  27653  pnt  27658  qabvle  27669  padicabv  27674  ostth1  27677  noextend  27711  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noeta2  27829  etasslt2  27859  leftf  27904  rightf  27905  lltropt  27911  sltlpss  27945  slelss  27946  negsproplem2  28061  negsid  28073  slemuld  28164  slemul1ad  28208  precsexlem11  28241  onaddscl  28286  onmulscl  28287  nohalf  28407  halfcut  28416  zs12bday  28424  istrkg2ld  28468  tgldimor  28510  motgrp  28551  perpln1  28718  perpln2  28719  isperp  28720  snstrvtxval  29054  snstriedgval  29055  isuhgrop  29087  uhgrunop  29092  uhgrstrrepe  29095  upgrop  29111  upgrunop  29136  umgrunop  29138  isusgrs  29173  isuspgrop  29178  isusgrop  29179  usgrop  29180  usgrstrrepe  29252  uspgr1ewop  29265  usgr2v1e2w  29269  uhgrspan1  29320  upgrres  29323  umgrres  29324  usgrres  29325  upgrres1  29330  umgrres1  29331  usgrres1  29332  isfusgrcl  29338  fusgredgfi  29342  usgr1v0e  29343  nbgrval  29353  nbusgrf1o1  29387  nbfusgrlevtxm2  29395  uvtx01vtx  29414  usgrexilem  29457  usgrexi  29458  cusgrexi  29460  structtousgr  29462  structtocusgr  29463  cusgrres  29466  cusgrfilem3  29475  sizusglecusg  29481  vtxdgfval  29485  vtxdgop  29488  vtxdgf  29489  vtxdlfgrval  29503  vtxd0nedgb  29506  vtxdusgr0edgnelALT  29514  1loopgrvd0  29522  1egrvtxdg1  29527  1egrvtxdg0  29529  p1evtxdeqlem  29530  p1evtxdeq  29531  p1evtxdp1  29532  umgr2v2e  29543  vdiscusgrb  29548  vdegp1ai  29554  vdegp1bi  29555  ewlkle  29623  wksfval  29627  wksvOLD  29638  wlk1ewlk  29658  uspgr2wlkeq  29664  wlkp1lem8  29698  dfpth2  29749  upgr2pthnlp  29752  wlkiswwlks2  29895  wlksnwwlknvbij  29928  2pthdlem1  29950  wpthswwlks2on  29981  elwwlks2  29986  elwspths2spth  29987  clwlkclwwlklem1  30018  clwwlknfi  30064  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlkvbij  30132  0wlkonlem1  30137  0wlkons1  30140  0pthon  30146  3wlkdlem4  30181  upgr3v3e3cycl  30199  trlsegvdeglem3  30241  trlsegvdeglem5  30243  eupth2lemb  30256  frgr3v  30294  frgr2wwlk1  30348  fusgreghash2wspv  30354  ex-lcm  30477  vsfval  30652  ipasslem7  30855  minvecolem2  30894  h2hcau  30998  h2hlm  30999  hlimadd  31212  hhsscms  31297  chocunii  31320  occllem  31322  eigposi  31855  leopnmid  32157  opsqrlem1  32159  hmopidmchi  32170  mdslj1i  32338  addltmulALT  32465  imadifxp  32614  2ndimaxp  32656  2ndresdju  32659  fressupp  32697  fsuppcurry1  32736  fsuppcurry2  32737  xaddeq0  32757  fzodif2  32793  pwrssmgc  32990  xrge0npcan  33025  gsumpart  33060  gsummulgc2  33063  gsumhashmul  33064  xrge0tsmsd  33065  gsumle  33101  symgcom  33103  cycpmfvlem  33132  cycpmfv3  33135  cycpmconjslem2  33175  elrgspnlem2  33247  rlocf1  33277  islinds5  33395  ellspds  33396  qusima  33436  qusrn  33437  nsgmgc  33440  zringfrac  33582  resssra  33638  exsslsb  33647  ply1degltdimlem  33673  ply1degltdim  33674  algextdeglem8  33765  2sqr3minply  33791  locfinreflem  33839  locfinref  33840  zarcmplem  33880  xpinpreima2  33906  cnre2csqlem  33909  tpr2rico  33911  ordtrestNEW  33920  ordtrest2NEW  33922  mndpluscn  33925  pnfneige0  33950  qqhghm  33989  qqhrhm  33990  qqhcn  33992  qqhucn  33993  rrhcn  33998  rrhre  34022  esumsplit  34054  esumpr  34067  esumfsup  34071  sigaclcu2  34121  pwsiga  34131  prsiga  34132  sigapildsys  34163  ldgenpisyslem1  34164  measvuni  34215  elmbfmvol2  34269  mbfmcnt  34270  sxbrsigalem1  34287  sxbrsiga  34292  omsfval  34296  carsgclctunlem2  34321  sibf0  34336  sitgclg  34344  sitmval  34351  eulerpartgbij  34374  eulerpartlemgh  34380  isrrvv  34445  rrvadd  34454  rrvmulc  34455  dstrvprob  34474  coinflipspace  34483  coinfliprv  34485  ballotlemfmpn  34497  ballotlem1ri  34537  sgnmulsgn  34552  plymul02  34561  signsplypnf  34565  signsply0  34566  signswrid  34573  prodfzo03  34618  itgexpif  34621  circlemethhgt  34658  hgt750lemb  34671  cardpred  35104  indispconn  35239  connpconn  35240  iccllysconn  35255  cvmopnlem  35283  cvmliftlem15  35303  cvmlift2lem3  35310  satfn  35360  satom  35361  satfv0  35363  ex-sategoelelomsuc  35431  prv0  35435  prv1n  35436  mrsubff  35517  mrsubccat  35523  circum  35679  elhf2  36176  bj-elid4  37169  bj-endbase  37317  bj-endcomp  37318  irrdifflemf  37326  topdifinfindis  37347  icoreelrn  37362  finxpreclem2  37391  finixpnum  37612  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem5  37632  poimirlem10  37637  poimirlem22  37649  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  dvtan  37677  itg2addnclem  37678  ftc1anclem5  37704  dvasin  37711  dvreasin  37713  dvreacos  37714  areacirclem1  37715  areacirc  37720  bnd2lem  37798  prdsbnd  37800  cntotbnd  37803  cnpwstotbnd  37804  isdrngo2  37965  prter2  38882  eqlkr2  39101  tendoidcl  40771  cdlemk56  40973  dihpN  41338  mapdhval  41726  hlhillcs  41964  lcmineqlem9  42038  redvmptabs  42390  readvrec2  42391  readvrec  42392  sn-00idlem3  42430  remul02  42435  remul01  42437  reixi  42452  remullid  42463  sn-0tie0  42469  mulgt0b2d  42490  sn-0lt1  42493  frlmvscadiccat  42516  fsuppind  42600  fsuppssind  42603  mhphflem  42606  mhphf  42607  mhphf2  42608  prjspreln0  42619  3cubes  42701  isnacs3  42721  diophrw  42770  lzenom  42781  diophin  42783  pellexlem5  42844  pw2f1ocnv  43049  dnnumch2  43057  kelac2lem  43076  kelac2  43077  dfac21  43078  pwfi2f1o  43108  frlmpwfi  43110  mpaaeu  43162  rngunsnply  43181  mendbas  43192  mendplusgfval  43193  mendmulrfval  43195  mendsca  43197  mendvscafval  43198  idomodle  43203  proot1ex  43208  deg1mhm  43212  onsupuni  43241  oninfint  43248  onsupmaxb  43251  limexissupab  43296  oaomoencom  43330  dflim5  43342  tfsconcatfv2  43353  ofoaid1  43371  ofoaid2  43372  naddcnff  43375  naddcnffo  43377  naddcnfid1  43380  naddcnfid2  43381  minregex2  43548  alephiso2  43571  trclubgNEW  43631  dmtrcl  43640  rntrcl  43641  brfvidRP  43701  trclrelexplem  43724  relexp01min  43726  trclimalb2  43739  dssmapfvd  44030  ntrk0kbimka  44052  ntrrn  44135  dssmapntrcls  44141  amgm2d  44211  amgm3d  44212  amgm4d  44213  hashnzfzclim  44341  ofsubid  44343  ofdivrec  44345  dvconstbi  44353  wessf1ornlem  45190  fzisoeu  45312  iuneqfzuzlem  45345  sumnnodd  45645  limsuppnfdlem  45716  liminfgf  45773  negcncfg  45896  cnfdmsn  45897  dvmptfprod  45960  itgcoscmulx  45984  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  stoweidlem42  46057  stoweidlem44  46059  stoweidlem48  46063  stoweidlem62  46077  stoweid  46078  stirlinglem7  46095  stirlinglem11  46099  stirlinglem12  46100  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem24  46146  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem70  46191  fourierdlem80  46201  fourierdlem83  46204  fourierdlem85  46206  fourierdlem102  46223  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem114  46235  etransclem18  46267  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem35  46284  etransclem46  46295  prsal  46333  ovolval5lem3  46669  fcoreslem3  47077  setsidel  47363  fundcmpsurbijinjpreimafv  47394  iccpartipre  47408  iccpartiltu  47409  sprval  47466  sprbisymrel  47486  prprval  47501  prprelprb  47504  fmtnoprmfac2lem1  47553  mod42tp1mod8  47589  sfprmdvdsmersenne  47590  perfectALTVlem2  47709  fpprel2  47728  stgoldbwt  47763  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem2  47793  clnbgrval  47809  isubgredgss  47851  isuspgrim0  47872  uspgrimprop  47873  grimcnv  47879  ushggricedg  47896  isubgrgrim  47897  grtriprop  47908  grtriclwlk3  47912  stgrvtx  47921  stgriedg  47922  stgrusgra  47926  isubgr3stgrlem2  47934  isubgr3stgrlem3  47935  isubgr3stgrlem7  47939  isubgr3stgrlem8  47940  grlicsym  47973  clnbgr3stgrgrlic  47979  usgrexmpl12ngrlic  47998  gpgvtx  48002  gpgiedg  48003  gpgusgra  48012  gpgorder  48013  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  upwlksfval  48051  uspgrbisymrelALT  48071  mgmplusgiopALT  48110  sgrp2sgrp  48144  zlidlring  48150  2zrngnmlid  48171  rngchomfvalALTV  48183  rngcidALTV  48190  rngcrescrhmALTV  48196  funcringcsetcALTV2lem8  48213  ringchomfvalALTV  48217  ringcidALTV  48224  funcringcsetclem8ALTV  48236  srhmsubcALTV  48241  fldcALTV  48248  altgsumbcALT  48269  zlmodzxzel  48271  zlmodzxzsubm  48275  zlmodzxzsub  48276  scmsuppss  48287  ply1mulgsum  48307  dmatALTbas  48318  lcoop  48328  lincval0  48332  lco0  48344  linds0  48382  snlindsntorlem  48387  lmod1lem2  48405  lmod1lem3  48406  lmod1zr  48410  lmod1zrnlvec  48411  zlmodzxznm  48414  zlmodzxzldeplem4  48420  expnegico01  48435  pw2m1lepw2m1  48437  fldivexpfllog2  48486  blennnelnn  48497  blenpw2  48499  nnpw2pmod  48504  blennnt2  48510  nnolog2flm1  48511  digfval  48518  dignnld  48524  dig2nn0ld  48525  0dig2nn0e  48533  0dig2nn0o  48534  1arymaptf1  48563  2arymaptf1  48574  itcovalendof  48590  itcovalt2lem1  48596  rrx2plordisom  48644  ehl2eudisval0  48646  rrxlines  48654  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrxsphere  48669  line2  48673  line2x  48675  line2y  48676  inlinecirc02preu  48709  joindm2  48865  meetdm2  48867  mndtcbasval  49177  amgmwlem  49321  amgmlemALT  49322  amgmw2d  49323