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  3838  relsnopg  5782  poirr2  6113  fvrnressn  7150  isomin  7329  isoini  7330  mptmpoopabbrdOLDOLD  8080  opco1  8120  opco2  8121  supp0  8162  suppval1  8163  suppssr  8192  dmtpos  8235  mpocurryd  8266  oaabs2  8659  elqsecl  8783  mapsncnv  8905  boxcutc  8953  domunsncan  9084  findcard2d  9178  unxpdom2  9260  sucxpdom  9261  ac6sfi  9290  imafi  9323  xpfiOLD  9329  snopfsupp  9401  fifo  9442  ordtypelem4  9533  oismo  9552  wofib  9557  brwdom2  9585  canthwdom  9591  cantnfval  9680  cantnflt  9684  cantnff  9686  cantnf0  9687  cantnflem1b  9698  cantnflem1  9701  cnfcom  9712  cnfcom2lem  9713  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  ranksnb  9839  updjudhcoinlf  9944  updjudhcoinrg  9945  updjud  9946  tskwe  9962  cardidm  9971  infxpenc  10030  fseqdom  10038  dfac8clem  10044  dfac12lem2  10157  infmap2  10229  fin23lem14  10345  fin23lem40  10363  isf34lem7  10391  isf34lem6  10392  fin1a2lem12  10423  hsmexlem4  10441  hsmexlem5  10442  ac5b  10490  alephexp1  10591  alephsuc3  10592  fpwwe2lem7  10649  fpwwe2lem12  10654  canthwe  10663  canthp1lem2  10665  gchdju1  10668  pwfseqlem5  10675  wunco  10745  prlem934  11045  supsrlem  11123  msqge0  11756  negfi  12189  ofnegsub  12236  ofsubge0  12237  xaddpnf1  13240  supxrmnf  13331  fz0sn0fz1  13660  injresinjlem  13801  fldiv4lem1div2  13852  uzindi  13998  seqfeq4  14067  seqof  14075  bcval5  14334  hashdomi  14396  hash1snb  14435  hashmap  14451  hashge2el2difr  14497  hashtpg  14501  fi1uzind  14523  ccatlen  14591  ccat0  14592  lswccatn0lsw  14607  ccatalpha  14609  s111  14631  ccat2s1fvw  14654  swrd0  14674  swrdwrdsymb  14678  swrdspsleq  14681  reps  14786  repsw0  14793  repswccat  14802  repswrevw  14803  lswcshw  14831  cshwsexaOLD  14841  scshwfzeqfzo  14843  lsws2  14921  lsws3  14922  lsws4  14923  wrdlen2i  14959  s2rn  14980  s3rn  14981  s7rn  14982  relexpsucnnr  15042  relexpaddg  15070  shftfib  15089  reusq0  15479  limsupcl  15487  limsupgf  15489  limsupval2  15494  isercolllem3  15681  modfsummods  15807  ackbijnn  15842  supcvg  15870  fprodfac  15987  fprodmodd  16011  fallfac0  16042  bpoly4  16073  ege2le3  16104  rpnnen2lem5  16234  ruclem11  16256  fsumdvds  16325  fproddvdsd  16352  mod2eq1n2dvds  16364  oddnn02np1  16365  oddge22np1  16366  evennn02n  16367  evennn2n  16368  bitsinv2  16460  sadaddlem  16483  smupf  16495  smup0  16496  smu01lem  16502  nn0rppwr  16578  3lcm2e6woprm  16632  6lcm4e12  16633  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  coprmprod  16678  ge2nprmge4  16718  isprm6  16731  hashdvds  16792  phisum  16808  reumodprminv  16822  prmreclem6  16939  vdwlem13  17011  ramtlecl  17018  0ram  17038  prmdvdsprmo  17060  fvprmselgcd1  17063  prmgaplcmlem1  17069  prmgaplem7  17075  prmgaplcm  17078  cshwshashnsame  17121  prmlem0  17123  wunndx  17212  prdsval  17467  xpsbas  17584  xpsadd  17586  xpsmul  17587  xpssca  17588  xpsvsca  17589  xpsless  17590  xpsle  17591  mreexexlem2d  17655  mreacs  17668  acsfn  17669  isofn  17786  cicsym  17815  cicer  17817  idfu2nd  17888  idfucl  17892  fucsect  17986  initoeu2lem1  18025  initoeu2lem2  18026  setccatid  18095  setcepi  18099  catchomfval  18113  estrccatid  18142  estrreslem1  18147  estrreslem2  18148  estrres  18149  funcestrcsetclem8  18157  fullestrcsetc  18161  embedsetcestrclem  18167  funcsetcestrclem8  18172  uncfval  18244  odulub  18415  odujoin  18416  oduglb  18417  odumeet  18418  isipodrs  18545  fpwipodrs  18548  isacs5lem  18553  idmgmhm  18677  idmhm  18771  submacs  18803  frmdup1  18840  efmndbas  18847  sursubmefmnd  18872  injsubmefmnd  18873  idresefmnd  18875  smndex1id  18887  mgmnsgrpex  18907  mulgneg2  19089  subgacs  19142  nsgacs  19143  1nsgtrivd  19155  idrespermg  19390  psgnunilem5  19473  psgnsn  19499  odf1o2  19552  frgpuplem  19751  cntrcmnd  19821  cygctb  19871  gsumpr  19934  gsumzunsnd  19935  gsum2dlem2  19950  gsummptnn0fz  19965  dprdsubg  20005  dmdprdsplit2lem  20026  dmdprdpr  20030  dprdpr  20031  dpjeq  20040  ablfac1eulem  20053  pgpfac1lem2  20056  pgpfaclem1  20062  prmgrpsimpgd  20095  ablsimpgprmd  20096  srgbinomlem4  20187  unitgrp  20341  isirred  20377  isrnghm  20399  brric  20462  isnzr2hash  20477  0ringnnzr  20483  0ring01eqbi  20490  dfrngc2  20586  rnghmsscmap2  20587  rnghmsscmap  20588  funcrngcsetcALT  20599  dfringc2  20615  rhmsscmap2  20616  rhmsscmap  20617  rhmsscrnghm  20623  rngcresringcat  20627  srhmsubc  20638  rngcrescrhm  20642  rhmsubclem3  20645  rng1nnzr  20733  fldc  20742  imadrhmcl  20755  subrgacs  20758  sdrgacs  20759  cntzsdrg  20760  mptscmfsupp0  20882  lssacs  20922  pwssplit1  21015  lbsextlem2  21118  lbsextlem3  21119  rlmlsm  21161  rnglidlmmgm  21204  xrsmcmn  21352  xrs1mnd  21370  xrs10  21371  gsumfsum  21400  zringlpir  21426  zringcyg  21428  pzriprnglem4  21443  zndvds  21508  regsumsupp  21580  frlmip  21736  uvcvv1  21747  lsslinds  21789  psrass1lem  21890  psrlidm  21920  resspsradd  21933  resspsrmul  21934  resspsrvsca  21935  mplcoe5lem  21995  ltbwe  22000  selvfval  22070  mhpvarcl  22084  psdmul  22102  coe1fsupp  22148  psropprmul  22171  coe1add  22199  coe1mul2lem1  22202  coe1tm  22208  cply1coe0bi  22238  evls1rhmlem  22257  evl1sca  22270  evl1var  22272  pf1mpf  22288  pf1ind  22291  evls1vsca  22309  evls1maplmhm  22313  matmulr  22374  ofco2  22387  mat0dimbas0  22402  mat1dimelbas  22407  mat1f1o  22414  dmatval  22428  scmatghm  22469  mavmul0  22488  mavmul0g  22489  m1detdiag  22533  mdetunilem9  22556  maducoeval2  22576  madugsum  22579  smadiadetlem0  22597  smadiadetlem1a  22599  smadiadetlem4  22605  smadiadetglem1  22607  smadiadetglem2  22608  smadiadetg  22609  cramer0  22626  cpmat  22645  mat2pmatfval  22659  cpm2mfval  22685  m2cpminvid2lem  22690  pmatcollpw3fi1lem2  22723  pmatcollpw3fi1  22724  idpm2idmp  22737  pm2mpmhmlem2  22755  chpmatfval  22766  chfacfscmulfsupp  22795  chfacfpmmulfsupp  22799  cpmidpmatlem2  22807  cpmadugsumlemF  22812  cpmidgsum2  22815  cpmadumatpolylem1  22817  cayhamlem3  22823  cayhamlem4  22824  indistopon  22937  mreclatdemoBAD  23032  mnfnei  23157  resthauslem  23299  sshauslem  23308  discmp  23334  connima  23361  1stcfb  23381  ptbasfi  23517  hauseqlcld  23582  xkoptsub  23590  xkofvcn  23620  idqtop  23642  tgqtop  23648  kqdisj  23668  xpstopnlem1  23745  xpstopnlem2  23747  ufildom1  23862  alexsubb  23982  alexsubALTlem3  23985  ptcmplem2  23989  ptcmplem3  23990  tmdgsum  24031  ustneism  24160  ustuqtop1  24178  iducn  24219  prdsmet  24307  imasdsf1olem  24310  xpsxmet  24317  xpsdsval  24318  xpsmet  24319  prdsbl  24428  met1stc  24458  prdsxmslem2  24466  xpsxms  24471  xpsms  24472  psmetutop  24504  dscmet  24509  nmoffn  24648  nmofval  24651  nmolb  24654  nmof  24656  cnbl0  24710  xrsmopn  24750  xrge0gsumle  24771  xrge0tsms  24772  negfcncf  24866  cnrehmeo  24900  cnrehmeoOLD  24901  lebnum  24912  xlebnum  24913  reparphti  24945  reparphtiOLD  24946  pcopt  24971  pcopt2  24972  pcorevcl  24974  pcorevlem  24975  pi1xfrval  25003  pi1xfrcnvlem  25005  pi1xfrcnv  25006  pi1cof  25008  pi1coval  25009  nmhmcn  25069  cphsubrglem  25127  csscld  25199  cmetcaulem  25238  cmpcmet  25269  csschl  25326  rrxplusgvscavalb  25345  rrxsca  25346  ehleudis  25368  divcncf  25398  ovolunlem1  25448  ovolicc2lem4  25471  ioovolcl  25521  ioorcl2  25523  uniioovol  25530  uniioombllem4  25537  uniioombllem5  25538  uniioombllem6  25539  dyadmbllem  25550  mbfsub  25613  itg1climres  25665  xrge0f  25682  itg2ge0  25686  itg20  25688  itg2monolem1  25701  itg2i1fseq2  25707  ibl0  25738  ellimc2  25828  limcflf  25832  dvreslem  25860  dvidlem  25866  dvmptresicc  25867  dvid  25869  cpnres  25889  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvfre  25905  dvexp  25907  dvrec  25909  dvmptid  25911  dvmptc  25912  dvmptntr  25925  dvexp3  25932  dvlipcn  25949  dveq0  25955  dv11cn  25956  lhop2  25970  ftc1a  25994  itgpowd  26007  tdeglem1  26013  tdeglem3  26014  tdeglem4  26015  tdeglem2  26016  mdeglt  26020  mdegxrcl  26022  mdegcl  26024  mdeg0  26025  mdegle0  26032  ply1remlem  26120  plypf1  26167  coe0  26211  dvply1  26241  elqaalem3  26279  aaliou2b  26299  aaliou3lem8  26303  aaliou3lem7  26307  taylfvallem  26315  taylf  26318  tayl0  26319  taylpfval  26322  taylply  26327  dvtaylp  26328  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem1  26359  ulmdvlem2  26360  ulmdvlem3  26361  radcnvcl  26376  psercnlem2  26384  psercn  26386  pserdv  26389  abelthlem3  26393  abelth  26401  sincn  26404  coscn  26405  reefgim  26410  tangtx  26464  pige3ALT  26479  cos02pilt1  26485  cosordlem  26489  logcn  26606  dvlog  26610  advlog  26613  advlogexp  26614  logtayl  26619  logccv  26622  dvcxp1  26699  dvcncxp1  26702  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  sqrtcn  26710  loglesqrt  26721  logbfval  26750  isosctrlem2  26779  dquartlem1  26811  quart  26821  atancj  26870  efiatan  26872  atantan  26883  atanbndlem  26885  atansopn  26892  dvatan  26895  atantayl  26897  leibpilem2  26901  leibpi  26902  log2tlbnd  26905  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  divsqrtsumlem  26940  jensenlem1  26947  jensenlem2  26948  jensen  26949  amgmlem  26950  amgm  26951  emcllem4  26959  emcllem7  26962  lgamcvg2  27015  gamcvg2lem  27019  wilthlem2  27029  wilthlem3  27030  basellem6  27046  chtrpcl  27135  ppiltx  27137  1sgm2ppw  27161  chtlepsi  27167  chpub  27181  logfacbnd3  27184  logfacrlim  27185  perfectlem2  27191  dchrelbas2  27198  dchrabs  27221  dchrhash  27232  bposlem7  27251  lgsdir2lem5  27290  lgsqrlem1  27307  gausslemma2dlem5  27332  gausslemma2dlem6  27333  lgseisenlem4  27339  lgsquad2lem1  27345  lgsquad3  27348  2sqreu  27417  2sqreunn  27418  2sqreult  27419  2sqreultb  27420  2sqreunnlt  27421  chpo1ub  27441  vmadivsumb  27444  rpvmasumlem  27448  dchrisumlem2  27451  dchrmusumlema  27454  dchrvmasumlem2  27459  dchrvmasumlema  27461  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0lem1  27477  rplogsum  27488  mudivsum  27491  logdivsum  27494  mulog2sumlem2  27496  vmalogdivsum2  27499  2vmadivsumlem  27501  log2sumbnd  27505  selberglem2  27507  selbergb  27510  selberg2lem  27511  selberg2b  27513  selberg3lem1  27518  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntibndlem1  27550  pntibndlem2  27552  pntibndlem3  27553  pntlemb  27558  pntlemr  27563  pntlemf  27566  pntlem3  27570  pnt  27575  qabvle  27586  padicabv  27591  ostth1  27594  noextend  27628  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noeta2  27746  etasslt2  27776  leftf  27821  rightf  27822  lltropt  27828  sltlpss  27862  slelss  27863  negsproplem2  27978  negsid  27990  slemuld  28081  slemul1ad  28125  precsexlem11  28158  onaddscl  28203  onmulscl  28204  nohalf  28324  halfcut  28333  zs12bday  28341  istrkg2ld  28385  tgldimor  28427  motgrp  28468  perpln1  28635  perpln2  28636  isperp  28637  snstrvtxval  28962  snstriedgval  28963  isuhgrop  28995  uhgrunop  29000  uhgrstrrepe  29003  upgrop  29019  upgrunop  29044  umgrunop  29046  isusgrs  29081  isuspgrop  29086  isusgrop  29087  usgrop  29088  usgrstrrepe  29160  uspgr1ewop  29173  usgr2v1e2w  29177  uhgrspan1  29228  upgrres  29231  umgrres  29232  usgrres  29233  upgrres1  29238  umgrres1  29239  usgrres1  29240  isfusgrcl  29246  fusgredgfi  29250  usgr1v0e  29251  nbgrval  29261  nbusgrf1o1  29295  nbfusgrlevtxm2  29303  uvtx01vtx  29322  usgrexilem  29365  usgrexi  29366  cusgrexi  29368  structtousgr  29370  structtocusgr  29371  cusgrres  29374  cusgrfilem3  29383  sizusglecusg  29389  vtxdgfval  29393  vtxdgop  29396  vtxdgf  29397  vtxdlfgrval  29411  vtxd0nedgb  29414  vtxdusgr0edgnelALT  29422  1loopgrvd0  29430  1egrvtxdg1  29435  1egrvtxdg0  29437  p1evtxdeqlem  29438  p1evtxdeq  29439  p1evtxdp1  29440  umgr2v2e  29451  vdiscusgrb  29456  vdegp1ai  29462  vdegp1bi  29463  ewlkle  29531  wksfval  29535  wksvOLD  29546  wlk1ewlk  29566  uspgr2wlkeq  29572  wlkp1lem8  29606  dfpth2  29657  upgr2pthnlp  29660  wlkiswwlks2  29803  wlksnwwlknvbij  29836  2pthdlem1  29858  wpthswwlks2on  29889  elwwlks2  29894  elwspths2spth  29895  clwlkclwwlklem1  29926  clwwlknfi  29972  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlkvbij  30040  0wlkonlem1  30045  0wlkons1  30048  0pthon  30054  3wlkdlem4  30089  upgr3v3e3cycl  30107  trlsegvdeglem3  30149  trlsegvdeglem5  30151  eupth2lemb  30164  frgr3v  30202  frgr2wwlk1  30256  fusgreghash2wspv  30262  ex-lcm  30385  vsfval  30560  ipasslem7  30763  minvecolem2  30802  h2hcau  30906  h2hlm  30907  hlimadd  31120  hhsscms  31205  chocunii  31228  occllem  31230  eigposi  31763  leopnmid  32065  opsqrlem1  32067  hmopidmchi  32078  mdslj1i  32246  addltmulALT  32373  imadifxp  32528  2ndimaxp  32570  2ndresdju  32573  fressupp  32611  fsuppcurry1  32648  fsuppcurry2  32649  xaddeq0  32676  fzodif2  32714  sgnmulsgn  32767  pwrssmgc  32926  xrge0npcan  32961  gsumpart  32997  gsummulgc2  33000  gsumhashmul  33001  xrge0tsmsd  33002  gsumle  33038  symgcom  33040  cycpmfvlem  33069  cycpmfv3  33072  cycpmconjslem2  33112  elrgspnlem2  33184  rlocf1  33214  islinds5  33328  ellspds  33329  qusima  33369  qusrn  33370  nsgmgc  33373  zringfrac  33515  resssra  33573  exsslsb  33582  ply1degltdimlem  33608  ply1degltdim  33609  algextdeglem8  33704  iconstr  33746  2sqr3minply  33760  cos9thpiminplylem1  33762  cos9thpiminply  33768  locfinreflem  33817  locfinref  33818  zarcmplem  33858  xpinpreima2  33884  cnre2csqlem  33887  tpr2rico  33889  ordtrestNEW  33898  ordtrest2NEW  33900  mndpluscn  33903  pnfneige0  33928  qqhghm  33965  qqhrhm  33966  qqhcn  33968  qqhucn  33969  rrhcn  33974  rrhre  33998  esumsplit  34030  esumpr  34043  esumfsup  34047  sigaclcu2  34097  pwsiga  34107  prsiga  34108  sigapildsys  34139  ldgenpisyslem1  34140  measvuni  34191  elmbfmvol2  34245  mbfmcnt  34246  sxbrsigalem1  34263  sxbrsiga  34268  omsfval  34272  carsgclctunlem2  34297  sibf0  34312  sitgclg  34320  sitmval  34327  eulerpartgbij  34350  eulerpartlemgh  34356  isrrvv  34421  rrvadd  34430  rrvmulc  34431  dstrvprob  34450  coinflipspace  34459  coinfliprv  34461  ballotlemfmpn  34473  ballotlem1ri  34513  plymul02  34524  signsplypnf  34528  signsply0  34529  signswrid  34536  prodfzo03  34581  itgexpif  34584  circlemethhgt  34621  hgt750lemb  34634  cardpred  35067  indispconn  35202  connpconn  35203  iccllysconn  35218  cvmopnlem  35246  cvmliftlem15  35266  cvmlift2lem3  35273  satfn  35323  satom  35324  satfv0  35326  ex-sategoelelomsuc  35394  prv0  35398  prv1n  35399  mrsubff  35480  mrsubccat  35486  circum  35642  elhf2  36139  bj-elid4  37132  bj-endbase  37280  bj-endcomp  37281  irrdifflemf  37289  topdifinfindis  37310  icoreelrn  37325  finxpreclem2  37354  finixpnum  37575  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem5  37595  poimirlem10  37600  poimirlem22  37612  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  poimirlem32  37622  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  dvtan  37640  itg2addnclem  37641  ftc1anclem5  37667  dvasin  37674  dvreasin  37676  dvreacos  37677  areacirclem1  37678  areacirc  37683  bnd2lem  37761  prdsbnd  37763  cntotbnd  37766  cnpwstotbnd  37767  isdrngo2  37928  prter2  38845  eqlkr2  39064  tendoidcl  40734  cdlemk56  40936  dihpN  41301  mapdhval  41689  hlhillcs  41923  lcmineqlem9  41996  redvmptabs  42350  readvrec2  42351  readvrec  42352  sn-00idlem3  42390  remul02  42395  remul01  42397  reixi  42412  remullid  42423  sn-0tie0  42429  mulgt0b2d  42450  sn-0lt1  42453  frlmvscadiccat  42476  fsuppind  42560  fsuppssind  42563  mhphflem  42566  mhphf  42567  mhphf2  42568  prjspreln0  42579  3cubes  42660  isnacs3  42680  diophrw  42729  lzenom  42740  diophin  42742  pellexlem5  42803  pw2f1ocnv  43008  dnnumch2  43016  kelac2lem  43035  kelac2  43036  dfac21  43037  pwfi2f1o  43067  frlmpwfi  43069  mpaaeu  43121  rngunsnply  43140  mendbas  43151  mendplusgfval  43152  mendmulrfval  43154  mendsca  43156  mendvscafval  43157  idomodle  43162  proot1ex  43167  deg1mhm  43171  onsupuni  43200  oninfint  43207  onsupmaxb  43210  limexissupab  43254  oaomoencom  43288  dflim5  43300  tfsconcatfv2  43311  ofoaid1  43329  ofoaid2  43330  naddcnff  43333  naddcnffo  43335  naddcnfid1  43338  naddcnfid2  43339  minregex2  43506  alephiso2  43529  trclubgNEW  43589  dmtrcl  43598  rntrcl  43599  brfvidRP  43659  trclrelexplem  43682  relexp01min  43684  trclimalb2  43697  dssmapfvd  43988  ntrk0kbimka  44010  ntrrn  44093  dssmapntrcls  44099  amgm2d  44169  amgm3d  44170  amgm4d  44171  hashnzfzclim  44294  ofsubid  44296  ofdivrec  44298  dvconstbi  44306  wessf1ornlem  45157  fzisoeu  45277  iuneqfzuzlem  45309  sumnnodd  45607  limsuppnfdlem  45678  liminfgf  45735  negcncfg  45858  cnfdmsn  45859  dvmptfprod  45922  itgcoscmulx  45946  stoweidlem13  45990  stoweidlem26  46003  stoweidlem34  46011  stoweidlem42  46019  stoweidlem44  46021  stoweidlem48  46025  stoweidlem62  46039  stoweid  46040  stirlinglem7  46057  stirlinglem11  46061  stirlinglem12  46062  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem24  46108  fourierdlem48  46131  fourierdlem49  46132  fourierdlem62  46145  fourierdlem70  46153  fourierdlem80  46163  fourierdlem83  46166  fourierdlem85  46168  fourierdlem102  46185  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem114  46197  etransclem18  46229  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem35  46246  etransclem46  46257  prsal  46295  ovolval5lem3  46631  fcoreslem3  47042  setsidel  47338  fundcmpsurbijinjpreimafv  47369  iccpartipre  47383  iccpartiltu  47384  sprval  47441  sprbisymrel  47461  prprval  47476  prprelprb  47479  fmtnoprmfac2lem1  47528  mod42tp1mod8  47564  sfprmdvdsmersenne  47565  perfectALTVlem2  47684  fpprel2  47703  stgoldbwt  47738  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem2  47768  clnbgrval  47784  isubgredgss  47826  grimcnv  47849  isuspgrim0  47855  ushggricedg  47888  isubgrgrim  47890  grtriprop  47901  grtriclwlk3  47905  stgrvtx  47914  stgriedg  47915  stgrusgra  47919  isubgr3stgrlem2  47927  isubgr3stgrlem3  47928  isubgr3stgrlem7  47932  isubgr3stgrlem8  47933  grlicsym  47966  clnbgr3stgrgrlic  47972  usgrexmpl12ngrlic  47991  gpgvtx  47995  gpgiedg  47996  gpgusgra  48009  gpgorder  48011  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  upwlksfval  48058  uspgrbisymrelALT  48078  mgmplusgiopALT  48117  sgrp2sgrp  48151  zlidlring  48157  2zrngnmlid  48178  rngchomfvalALTV  48190  rngcidALTV  48197  rngcrescrhmALTV  48203  funcringcsetcALTV2lem8  48220  ringchomfvalALTV  48224  ringcidALTV  48231  funcringcsetclem8ALTV  48243  srhmsubcALTV  48248  fldcALTV  48255  altgsumbcALT  48276  zlmodzxzel  48278  zlmodzxzsubm  48282  zlmodzxzsub  48283  scmsuppss  48294  ply1mulgsum  48314  dmatALTbas  48325  lcoop  48335  lincval0  48339  lco0  48351  linds0  48389  snlindsntorlem  48394  lmod1lem2  48412  lmod1lem3  48413  lmod1zr  48417  lmod1zrnlvec  48418  zlmodzxznm  48421  zlmodzxzldeplem4  48427  expnegico01  48442  pw2m1lepw2m1  48444  fldivexpfllog2  48493  blennnelnn  48504  blenpw2  48506  nnpw2pmod  48511  blennnt2  48517  nnolog2flm1  48518  digfval  48525  dignnld  48531  dig2nn0ld  48532  0dig2nn0e  48540  0dig2nn0o  48541  1arymaptf1  48570  2arymaptf1  48581  itcovalendof  48597  itcovalt2lem1  48603  rrx2plordisom  48651  ehl2eudisval0  48653  rrxlines  48661  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrxsphere  48676  line2  48680  line2x  48682  line2y  48683  inlinecirc02preu  48716  joindm2  48890  meetdm2  48892  invfn  48948  relcic  48960  discthing  49295  idfudiag1  49358  mndtcbasval  49405  amgmwlem  49614  amgmlemALT  49615  amgmw2d  49616