Theorem mp1i 14

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 ⊢ (𝜒 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6

This theorem is used by:  sbcg  3811  relsnopg  5784  poirr2  6118  fvrnressn  7158  isomin  7338  isoini  7339  opco1  8120  opco2  8121  supp0  8163  suppval1  8164  suppssr  8193  dmtpos  8236  mpocurryd  8267  oaabs2  8637  elqsecl  8766  mapsncnv  8900  boxcutc  8948  domunsncan  9075  findcard2d  9161  unxpdom2  9230  sucxpdom  9231  ac6sfi  9254  imafi  9285  snopfsupp  9361  fifo  9402  ordtypelem4  9493  oismo  9512  wofib  9517  brwdom2  9545  canthwdom  9551  cantnfval  9647  cantnflt  9651  cantnff  9653  cantnf0  9654  cantnflem1b  9665  cantnflem1  9668  cnfcom  9679  cnfcom2lem  9680  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  ranksnb  9809  updjudhcoinlf  9937  updjudhcoinrg  9938  updjud  9939  tskwe  9955  cardidm  9964  infxpenc  10021  fseqdom  10029  dfac8clem  10035  dfac12lem2  10147  infmap2  10219  fin23lem14  10335  fin23lem40  10353  isf34lem7  10381  isf34lem6  10382  fin1a2lem12  10413  hsmexlem4  10431  hsmexlem5  10432  ac5b  10480  alephexp1  10588  alephsuc3  10589  fpwwe2lem7  10646  fpwwe2lem12  10651  canthwe  10660  canthp1lem2  10662  gchdju1  10665  pwfseqlem5  10672  wunco  10742  prlem934  11042  supsrlem  11120  msqge0  11759  negfi  12188  ofnegsub  12240  ofsubge0  12241  xaddpnf1  13278  supxrmnf  13369  nnge2recico01  13560  fz0sn0fz1  13700  injresinjlem  13846  fldiv4lem1div2  13898  uzindi  14046  seqfeq4  14115  seqof  14123  bcval5  14382  hashdomi  14444  hash1snb  14484  hashmap  14500  hashge2el2difr  14546  hashtpg  14550  fi1uzind  14572  ccatlen  14640  ccat0  14641  lswccatn0lsw  14658  ccatalpha  14660  s111  14683  ccat2s1fvw  14706  swrd0  14728  swrdwrdsymb  14732  swrdspsleq  14735  reps  14841  repsw0  14848  repswccat  14857  repswrevw  14858  lswcshw  14886  scshwfzeqfzo  14897  lsws2  14975  lsws3  14976  lsws4  14977  wrdlen2i  15013  s2rn  15036  s3rn  15037  s7rn  15038  relexpsucnnr  15098  relexpaddg  15126  shftfib  15145  sgnmulsgn  15182  reusq0  15552  limsupcl  15560  limsupgf  15562  limsupval2  15567  isercolllem3  15754  modfsummods  15880  ackbijnn  15917  supcvg  15945  fprodfac  16060  fprodmodd  16084  fallfac0  16114  bpoly4  16145  ege2le3  16176  rpnnen2lem5  16306  ruclem11  16328  fsumdvds  16398  fproddvdsd  16425  mod2eq1n2dvds  16437  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  bitsinv2  16533  sadaddlem  16556  smupf  16568  smup0  16569  smu01lem  16575  nn0rppwr  16651  3lcm2e6woprm  16705  6lcm4e12  16706  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2  16730  coprmprod  16751  ge2nprmge4  16792  isprm6  16805  hashdvds  16866  phisum  16882  reumodprminv  16896  prmreclem6  17013  vdwlem13  17085  ramtlecl  17092  0ram  17112  prmdvdsprmo  17134  fvprmselgcd1  17137  prmgaplcmlem1  17143  prmgaplem7  17149  prmgaplcm  17152  cshwshashnsame  17195  prmlem0  17197  wunndx  17287  prdsval  17540  xpsbas  17658  xpsadd  17660  xpsmul  17661  xpssca  17662  xpsvsca  17663  xpsless  17664  xpsle  17665  mreexexlem2d  17733  mreacs  17746  acsfn  17747  isofn  17864  cicsym  17893  cicer  17895  idfu2nd  17966  idfucl  17970  fucsect  18064  initoeu2lem1  18103  initoeu2lem2  18104  setccatid  18173  setcepi  18177  catchomfval  18191  estrccatid  18220  estrreslem1  18225  estrreslem2  18226  estrres  18227  funcestrcsetclem8  18235  fullestrcsetc  18239  embedsetcestrclem  18245  funcsetcestrclem8  18250  uncfval  18322  odulub  18493  odujoin  18494  oduglb  18495  odumeet  18496  isipodrs  18625  fpwipodrs  18628  isacs5lem  18633  idressidex0  18773  idmgmhm  18803  idmhm  18903  submacs  18936  frmdup1  18973  efmndbas  18980  sursubmefmnd  19005  injsubmefmnd  19006  idresefmnd  19008  smndex1id  19023  mgmnsgrpex  19043  mulgneg2  19231  subgacs  19284  nsgacs  19285  1nsgtrivd  19297  idrespermg  19538  psgnunilem5  19621  psgnsn  19647  odf1o2  19700  frgpuplem  19899  cntrcmnd  19969  cygctb  20019  gsumpr  20082  gsumzunsnd  20083  gsum2dlem2  20098  gsummptnn0fz  20113  dprdsubg  20153  dmdprdsplit2lem  20174  dmdprdpr  20178  dprdpr  20179  dpjeq  20188  ablfac1eulem  20201  pgpfac1lem2  20204  pgpfaclem1  20210  prmgrpsimpgd  20243  ablsimpgprmd  20244  gsumle  20272  srgbinomlem4  20368  unitgrp  20524  isirred  20560  isrnghm  20582  brric  20656  isnzr2hash  20680  0ringnnzr  20686  0ring01eqbi  20694  dfrngc2  20790  rnghmsscmap2  20791  rnghmsscmap  20792  funcrngcsetcALT  20803  dfringc2  20819  rhmsscmap2  20820  rhmsscmap  20821  rhmsscrnghm  20827  rngcresringcat  20831  srhmsubc  20842  rngcrescrhm  20846  rhmsubclem3  20849  rng1nnzr  20942  fldc  20950  imadrhmcl  20963  subrgacs  20966  sdrgacs  20967  cntzsdrg  20968  mptscmfsupp0  21111  lssacs  21151  pwssplit1  21243  lbsextlem2  21346  lbsextlem3  21347  rlmlsm  21389  rnglidlmmgm  21442  xrsmcmn  21608  gsumfsum  21647  xrs1mnd  21653  xrs10  21654  zringlpir  21680  zringcyg  21682  pzriprnglem4  21697  zndvds  21762  regsumsupp  21835  frlmip  21991  uvcvv1  22002  lsslinds  22044  psrass1lem  22148  psrlidm  22176  resspsradd  22189  resspsrmul  22190  resspsrvsca  22191  mplcoe5lem  22255  ltbwe  22260  selvfval  22335  mhpvarcl  22376  psdmul  22394  coe1fsupp  22439  psropprmul  22462  coe1add  22490  coe1mul2lem1  22493  coe1tm  22499  cply1coe0bi  22527  evls1rhmlem  22546  evl1sca  22559  evl1var  22561  pf1mpf  22577  pf1ind  22580  evls1vsca  22598  evls1maplmhm  22602  matmulr  22660  ofco2  22673  mat0dimbas0  22688  mat1dimelbas  22693  mat1f1o  22700  dmatval  22714  scmatghm  22755  mavmul0  22774  mavmul0g  22775  m1detdiag  22819  mdetunilem9  22842  maducoeval2  22862  madugsum  22865  smadiadetlem0  22883  smadiadetlem1a  22885  smadiadetlem4  22891  smadiadetglem1  22893  smadiadetglem2  22894  smadiadetg  22895  matunitlindflem1  22901  matunitlindflem2  22902  cramer0  22915  cpmat  22934  mat2pmatfval  22948  cpm2mfval  22974  m2cpminvid2lem  22979  pmatcollpw3fi1lem2  23012  pmatcollpw3fi1  23013  idpm2idmp  23026  pm2mpmhmlem2  23044  chpmatfval  23055  chfacfscmulfsupp  23084  chfacfpmmulfsupp  23088  cpmidpmatlem2  23096  cpmadugsumlemF  23101  cpmidgsum2  23104  cpmadumatpolylem1  23106  cayhamlem3  23112  cayhamlem4  23113  indistopon  23226  mreclatdemoBAD  23321  mnfnei  23446  resthauslem  23588  sshauslem  23597  discmp  23623  connima  23650  1stcfb  23670  ptbasfi  23807  hauseqlcld  23872  xkoptsub  23880  xkofvcn  23910  idqtop  23932  tgqtop  23938  kqdisj  23958  xpstopnlem1  24035  xpstopnlem2  24037  ufildom1  24152  alexsubb  24272  alexsubALTlem3  24275  ptcmplem2  24279  ptcmplem3  24280  tmdgsum  24321  ustneism  24450  ustuqtop1  24467  iducn  24508  prdsmet  24596  imasdsf1olem  24599  xpsxmet  24606  xpsdsval  24607  xpsmet  24608  prdsbl  24717  met1stc  24747  prdsxmslem2  24755  xpsxms  24760  xpsms  24761  psmetutop  24793  dscmet  24798  nmoffn  24937  nmofval  24940  nmolb  24943  nmof  24945  cnbl0  24999  xrsmopn  25039  xrge0gsumle  25060  xrge0tsms  25061  negfcncf  25151  cnrehmeo  25181  lebnum  25192  xlebnum  25193  reparphti  25225  pcopt  25250  pcopt2  25251  pcorevcl  25253  pcorevlem  25254  pi1xfrval  25282  pi1xfrcnvlem  25284  pi1xfrcnv  25285  pi1cof  25287  pi1coval  25288  nmhmcn  25348  cphsubrglem  25405  csscld  25477  cmetcaulem  25516  cmpcmet  25547  csschl  25604  rrxplusgvscavalb  25623  rrxsca  25624  ehleudis  25646  divcncf  25675  ovolunlem1  25725  ovolicc2lem4  25748  ioovolcl  25798  ioorcl2  25800  uniioovol  25807  uniioombllem4  25814  uniioombllem5  25815  uniioombllem6  25816  dyadmbllem  25827  mbfsub  25890  itg1climres  25942  xrge0f  25959  itg2ge0  25963  itg20  25965  itg2monolem1  25978  itg2i1fseq2  25984  ibl0  26014  ellimc2  26104  limcflf  26108  dvreslem  26136  dvidlem  26142  dvmptresicc  26143  dvid  26145  cpnres  26164  dvaddbr  26165  dvmulbr  26166  dvfre  26178  dvexp  26180  dvrec  26182  dvmptid  26184  dvmptc  26185  dvmptntr  26198  dvexp3  26205  dvlipcn  26221  dveq0  26227  dv11cn  26228  lhop2  26242  ftc1a  26264  itgpowd  26277  tdeglem1  26283  tdeglem3  26284  tdeglem4  26285  tdeglem2  26286  mdeglt  26290  mdegxrcl  26292  mdegcl  26294  mdeg0  26295  mdegle0  26302  ply1remlem  26390  plypf1  26438  coe0  26482  plymul02  26510  dvply1  26514  elqaalem3  26553  aaliou2b  26577  aaliou3lem8  26581  aaliou3lem7  26585  taylfvallem  26594  taylf  26597  tayl0  26598  taylpfval  26601  taylply  26605  dvtaylp  26606  taylthlem1  26609  taylthlem2  26610  ulmdvlem1  26636  ulmdvlem2  26637  ulmdvlem3  26638  radcnvcl  26653  psercnlem2  26660  psercn  26662  pserdv  26665  abelthlem3  26669  abelth  26677  sincn  26680  coscn  26681  reefgim  26686  tangtx  26743  pige3ALT  26757  cos02pilt1  26763  cosordlem  26767  logcn  26884  dvlog  26888  advlog  26891  advlogexp  26892  logtayl  26897  logccv  26900  dvcxp1  26977  dvcncxp1  26980  cxpcn3lem  26984  cxpcn3  26985  resqrtcn  26986  sqrtcn  26987  loglesqrt  26998  logbfval  27027  isosctrlem2  27056  dquartlem1  27088  quart  27098  atancj  27147  efiatan  27149  atantan  27160  atanbndlem  27162  atansopn  27169  dvatan  27172  atantayl  27174  leibpilem2  27178  leibpi  27179  log2tlbnd  27182  rlimcnp2  27203  efrlim  27206  divsqrtsumlem  27216  jensenlem1  27223  jensenlem2  27224  jensen  27225  amgmlem  27226  amgm  27227  emcllem4  27235  emcllem7  27238  lgamcvg2  27291  gamcvg2lem  27295  wilthlem2  27305  wilthlem3  27306  basellem6  27322  chtrpcl  27411  ppiltx  27413  1sgm2ppw  27436  chtlepsi  27442  chpub  27456  logfacbnd3  27459  logfacrlim  27460  perfectlem2  27466  dchrelbas2  27473  dchrabs  27496  dchrhash  27507  bposlem7  27526  lgsdir2lem5  27565  lgsqrlem1  27582  gausslemma2dlem5  27607  gausslemma2dlem6  27608  lgseisenlem4  27614  lgsquad2lem1  27620  lgsquad3  27623  2sqreu  27692  2sqreunn  27693  2sqreult  27694  2sqreultb  27695  2sqreunnlt  27696  chpo1ub  27716  vmadivsumb  27719  rpvmasumlem  27723  dchrisumlem2  27726  dchrmusumlema  27729  dchrvmasumlem2  27734  dchrvmasumlema  27736  dchrvmasumiflem1  27737  dchrisum0flblem1  27744  dchrisum0lem1  27752  rplogsum  27763  mudivsum  27766  logdivsum  27769  mulog2sumlem2  27771  vmalogdivsum2  27774  2vmadivsumlem  27776  log2sumbnd  27780  selberglem2  27782  selbergb  27785  selberg2lem  27786  selberg2b  27788  selberg3lem1  27793  selberg4lem1  27796  selberg4  27797  pntrsumo1  27801  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntibndlem1  27825  pntibndlem2  27827  pntibndlem3  27828  pntlemb  27833  pntlemr  27838  pntlemf  27841  pntlem3  27845  pnt  27850  qabvle  27861  padicabv  27866  ostth1  27869  noextend  27902  nosupbnd2lem1  27951  noinfbnd2lem1  27966  noeta2  28026  etaslts2  28059  cutneg  28081  rightge0  28086  leftf  28120  rightf  28121  lltr  28127  ltslpss  28173  leslss  28174  negsproplem2  28294  negsid  28306  lemulsd  28403  lemuls1ad  28447  precsexlem11  28482  oncutlt  28529  onaddscl  28542  onmulscl  28543  onsbnd  28546  n0cut  28599  halfcut  28723  z12bdaylem1  28735  istrkg2ld  28801  tgldimor  28844  motgrp  28885  perpln1  29064  perpln2  29065  isperp  29066  angmgmlem  29274  angmgmbas  29277  snstrvtxval  29494  snstriedgval  29495  isuhgrop  29527  uhgrunop  29532  uhgrstrrepe  29535  upgrop  29551  upgrunop  29576  umgrunop  29578  isusgrs  29616  isuspgrop  29621  isusgrop  29622  usgrop  29623  usgrstrrepe  29695  uspgr1ewop  29708  usgr2v1e2w  29712  uhgrspan1  29763  upgrres  29766  umgrres  29767  usgrres  29768  upgrres1  29773  umgrres1  29774  usgrres1  29775  isfusgrcl  29781  fusgredgfi  29785  usgr1v0e  29786  nbgrval  29796  nbusgrf1o1  29830  nbfusgrlevtxm2  29838  uvtx01vtx  29857  usgrexilem  29900  usgrexi  29901  cusgrexi  29903  structtousgr  29905  structtocusgr  29906  cusgrres  29908  cusgrfilem3  29917  sizusglecusg  29923  vtxdgfval  29927  vtxdgop  29930  vtxdgf  29931  vtxdlfgrval  29945  vtxd0nedgb  29948  vtxdusgr0edgnelALT  29956  1loopgrvd0  29964  1egrvtxdg1  29969  1egrvtxdg0  29971  p1evtxdeqlem  29972  p1evtxdeq  29973  p1evtxdp1  29974  umgr2v2e  29985  vdiscusgrb  29990  vdegp1ai  29996  vdegp1bi  29997  ewlkle  30065  wksfval  30069  wlk1ewlk  30099  uspgr2wlkeq  30105  wlkp1lem8  30138  dfpth2  30193  upgr2pthnlp  30197  cyclnumvtx  30267  wlkiswwlks2  30343  wlksnwwlknvbij  30376  2pthdlem1  30398  wpthswwlks2on  30432  elwwlks2  30437  elwspths2spth  30438  clwlkclwwlklem1  30469  clwwlknfi  30515  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  clwwlkvbij  30583  0wlkonlem1  30588  0wlkons1  30591  0pthon  30597  3wlkdlem4  30642  upgr3v3e3cycl  30660  trlsegvdeglem3  30702  trlsegvdeglem5  30704  eupth2lemb  30717  frgr3v  30755  frgr2wwlk1  30809  fusgreghash2wspv  30815  ex-lcm  30938  vsfval  31114  ipasslem7  31317  minvecolem2  31356  h2hcau  31460  h2hlm  31461  hlimadd  31674  hhsscms  31759  chocunii  31782  occllem  31784  eigposi  32317  leopnmid  32619  opsqrlem1  32621  hmopidmchi  32632  mdslj1i  32800  addltmulALT  32927  imadifxp  33074  2ndimaxp  33119  2ndresdju  33122  fressupp  33160  fsuppcurry1  33195  fsuppcurry2  33196  xaddeq0  33224  fzodif2  33262  indfsid  33315  pwrssmgc  33440  xrge0npcan  33460  gsumpart  33503  gsummulgc2  33506  gsumhashmul  33507  xrge0tsmsd  33513  symgcom  33523  cycpmfvlem  33552  cycpmfv3  33555  cycpmconjslem2  33595  elrgspnlem2  33683  rlocf1  33714  islinds5  33802  ellspds  33803  qusima  33837  qusrn  33838  nsgmgc  33841  zringfrac  33964  selvply1rhmlemb  34029  selvply1rhmlem2  34031  esplyfval2  34075  esplyfval1  34083  esplyfvaln  34084  vieta  34090  resssra  34097  exsslsb  34107  ply1degltdimlem  34132  ply1degltdim  34133  algextdeglem8  34234  iconstr  34276  2sqr3minply  34290  cos9thpiminplylem1  34292  cos9thpiminply  34298  locfinreflem  34350  locfinref  34351  zarcmplem  34391  xpinpreima2  34417  cnre2csqlem  34420  tpr2rico  34422  ordtrestNEW  34431  ordtrest2NEW  34433  mndpluscn  34436  pnfneige0  34461  qqhghm  34498  qqhrhm  34499  qqhcn  34501  qqhucn  34502  rrhcn  34507  rrhre  34531  esumsplit  34563  esumpr  34576  esumfsup  34580  sigaclcu2  34630  pwsiga  34640  prsiga  34641  sigapildsys  34673  ldgenpisyslem1  34674  measvuni  34725  elmbfmvol2  34778  mbfmcnt  34779  sxbrsigalem1  34796  sxbrsiga  34801  omsfval  34805  carsgclctunlem2  34830  sibf0  34845  sitgclg  34853  sitmval  34860  eulerpartgbij  34883  eulerpartlemgh  34889  isrrvv  34954  rrvadd  34963  rrvmulc  34964  dstrvprob  34983  coinflipspace  34992  coinfliprv  34994  ballotlemfmpn  35006  ballotlem1ri  35046  signsplypnf  35058  signsply0  35059  signswrid  35066  prodfzo03  35111  itgexpif  35114  circlemethhgt  35151  hgt750lemb  35164  cardpred  35597  rankval4b  35607  indispconn  35813  connpconn  35814  iccllysconn  35829  cvmopnlem  35857  cvmliftlem15  35877  cvmlift2lem3  35884  satfn  35934  satom  35935  satfv0  35937  ex-sategoelelomsuc  36005  prv0  36009  prv1n  36010  mrsubff  36091  mrsubccat  36097  circum  36253  elhf2  36755  bj-elid4  37920  bj-endbase  38068  bj-endcomp  38069  irrdifflemf  38077  qdiff  38079  topdifinfindis  38100  icoreelrn  38115  finxpreclem2  38144  finixpnum  38359  poimirlem5  38374  poimirlem10  38379  poimirlem22  38391  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  poimirlem29  38398  poimirlem31  38400  poimirlem32  38401  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  dvtan  38419  itg2addnclem  38420  ftc1anclem5  38446  dvasin  38453  dvreasin  38455  dvreacos  38456  areacirclem1  38457  areacirc  38462  bnd2lem  38541  prdsbnd  38543  cntotbnd  38546  cnpwstotbnd  38547  isdrngo2  38708  prter2  39754  eqlkr2  39973  tendoidcl  41642  cdlemk56  41844  dihpN  42209  mapdhval  42597  hlhillcs  42831  lcmineqlem9  42903  redvmptabs  43235  readvrec2  43236  readvrec  43237  remul02  43280  remul01  43282  reixi  43298  remullid  43309  sn-0tie0  43339  mulgt0b1d  43360  sn-0lt1  43363  frlmvscadiccat  43394  fsuppind  43436  fsuppssind  43439  mhphflem  43442  mhphf  43443  mhphf2  43444  prjspreln0  43455  3cubes  43535  isnacs3  43555  diophrw  43604  lzenom  43615  diophin  43617  pellexlem5  43674  pw2f1ocnv  43878  dnnumch2  43886  kelac2lem  43905  kelac2  43906  dfac21  43907  pwfi2f1o  43937  frlmpwfi  43939  mpaaeu  43991  rngunsnply  44010  mendbas  44021  mendplusgfval  44022  mendmulrfval  44024  mendsca  44026  mendvscafval  44027  idomodle  44032  proot1ex  44037  deg1mhm  44041  onsupuni  44070  oninfint  44077  onsupmaxb  44080  limexissupab  44124  oaomoencom  44158  dflim5  44170  tfsconcatfv2  44181  ofoaid1  44199  ofoaid2  44200  naddcnff  44203  naddcnffo  44205  naddcnfid1  44208  naddcnfid2  44209  minregex2  44375  alephiso2  44398  trclubgNEW  44458  dmtrcl  44467  rntrcl  44468  brfvidRP  44528  trclrelexplem  44551  relexp01min  44553  trclimalb2  44566  dssmapfvd  44857  ntrk0kbimka  44879  ntrrn  44962  dssmapntrcls  44968  amgm2d  45038  amgm3d  45039  amgm4d  45040  hashnzfzclim  45146  ofsubid  45148  ofdivrec  45150  dvconstbi  45158  wessf1ornlem  46017  fzisoeu  46133  iuneqfzuzlem  46164  sumnnodd  46460  limsuppnfdlem  46529  liminfgf  46586  negcncfg  46709  cnfdmsn  46710  dvmptfprod  46773  itgcoscmulx  46797  stoweidlem13  46841  stoweidlem26  46854  stoweidlem34  46862  stoweidlem42  46870  stoweidlem44  46872  stoweidlem48  46876  stoweidlem62  46890  stoweid  46891  stirlinglem7  46908  stirlinglem11  46912  stirlinglem12  46913  dirkeritg  46930  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem24  46959  fourierdlem48  46982  fourierdlem49  46983  fourierdlem62  46996  fourierdlem70  47004  fourierdlem80  47014  fourierdlem83  47017  fourierdlem85  47019  fourierdlem102  47036  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fourierdlem114  47048  etransclem18  47080  etransclem23  47085  etransclem24  47086  etransclem25  47087  etransclem35  47097  etransclem46  47108  prsal  47146  ovolval5lem3  47482  preimaleiinlt  47549  chnsuslle  47709  chnerlem1  47710  fcoreslem3  47953  flmrecm1  48231  nndivides2  48272  setsidel  48276  fundcmpsurbijinjpreimafv  48307  iccpartipre  48321  iccpartiltu  48322  sprval  48379  sprbisymrel  48399  prprval  48414  prprelprb  48417  fmtnoprmfac2lem1  48469  mod42tp1mod8  48505  sfprmdvdsmersenne  48506  ppivalnnprm  48528  perfectALTVlem2  48638  fpprel2  48657  stgoldbwt  48692  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbndlem2  48722  clnbgrval  48738  isubgredgss  48781  grimcnv  48804  isuspgrim0  48810  ushggricedg  48843  isubgrgrim  48845  grtriprop  48857  grtriclwlk3  48861  stgrvtx  48870  stgriedg  48871  stgrusgra  48875  isubgr3stgrlem2  48883  isubgr3stgrlem3  48884  isubgr3stgrlem7  48888  isubgr3stgrlem8  48889  grlicsym  48929  clnbgr3stgrgrlic  48936  usgrexmpl12ngrlic  48955  gpgvtx  48959  gpgiedg  48960  gpgusgra  48973  gpgorder  48975  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedgiov  48981  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg5edgnedg  49046  grlimedgnedg  49047  upwlksfval  49051  uspgrbisymrelALT  49071  mgmplusgiopALT  49109  sgrp2sgrp  49143  zlidlring  49149  2zrngnmlid  49170  rngchomfvalALTV  49182  rngcidALTV  49189  rngcrescrhmALTV  49195  funcringcsetcALTV2lem8  49212  ringchomfvalALTV  49216  ringcidALTV  49223  funcringcsetclem8ALTV  49235  srhmsubcALTV  49240  fldcALTV  49247  altgsumbcALT  49283  zlmodzxzel  49285  zlmodzxzsubm  49289  zlmodzxzsub  49290  scmsuppss  49301  ply1mulgsum  49320  dmatALTbas  49331  lcoop  49341  lincval0  49345  lco0  49357  linds0  49395  snlindsntorlem  49400  lmod1lem2  49418  lmod1lem3  49419  lmod1zr  49423  lmod1zrnlvec  49424  zlmodzxznm  49427  zlmodzxzldeplem4  49433  expnegico01  49448  pw2m1lepw2m1  49450  fldivexpfllog2  49495  blennnelnn  49506  blenpw2  49508  nnpw2pmod  49513  blennnt2  49519  nnolog2flm1  49520  digfval  49527  dignnld  49533  dig2nn0ld  49534  0dig2nn0e  49542  0dig2nn0o  49543  1arymaptf1  49572  2arymaptf1  49583  itcovalendof  49599  itcovalt2lem1  49605  rrx2plordisom  49653  ehl2eudisval0  49655  rrxlines  49663  eenglngeehlnmlem1  49667  eenglngeehlnmlem2  49668  rrxsphere  49678  line2  49682  line2x  49684  line2y  49685  inlinecirc02preu  49718  joindm2  49894  meetdm2  49896  invfn  49956  relcic  49971  discthing  50387  idfudiag1  50451  mndtcbasval  50506  veroquaddetzerod  50819  amgmwlem  50820  amgmlemALT  50821  amgmw2d  50822