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:  relsnopg  5640  poirr2  5951  fvrnressn  6900  isomin  7069  isoini  7070  mptmpoopabbrd  7761  supp0  7818  suppval1  7819  suppssr  7844  dmtpos  7887  mpocurryd  7918  oaabs2  8255  elqsecl  8334  mapsncnv  8440  boxcutc  8488  domunsncan  8600  unxpdom2  8710  sucxpdom  8711  findcard2d  8744  ac6sfi  8746  xpfi  8773  imafi  8801  snopfsupp  8840  fifo  8880  ordtypelem4  8969  oismo  8988  wofib  8993  brwdom2  9021  canthwdom  9027  cantnfval  9115  cantnflt  9119  cantnff  9121  cantnf0  9122  cantnflem1b  9133  cantnflem1  9136  cnfcom  9147  cnfcom2lem  9148  ranksnb  9240  updjudhcoinlf  9345  updjudhcoinrg  9346  updjud  9347  tskwe  9363  cardidm  9372  infxpenc  9429  fseqdom  9437  dfac8clem  9443  dfac12lem2  9555  infmap2  9629  fin23lem14  9744  fin23lem40  9762  isf34lem7  9790  isf34lem6  9791  fin1a2lem12  9822  hsmexlem4  9840  hsmexlem5  9841  ac5b  9889  alephexp1  9990  alephsuc3  9991  fpwwe2lem8  10048  fpwwe2lem13  10053  canthwe  10062  canthp1lem2  10064  gchdju1  10067  pwfseqlem5  10074  wunco  10144  prlem934  10444  supsrlem  10522  msqge0  11150  negfi  11577  ofnegsub  11623  ofsubge0  11624  xaddpnf1  12607  supxrmnf  12698  fz0sn0fz1  13019  injresinjlem  13152  fldiv4lem1div2  13202  uzindi  13345  seqfeq4  13415  seqof  13423  bcval5  13674  hashdomi  13737  hash1snb  13776  hashmap  13792  hashge2el2difr  13835  hashtpg  13839  fi1uzind  13851  ccatlen  13918  ccatlenOLD  13919  ccat0  13920  lswccatn0lsw  13936  ccatalpha  13938  s111  13960  ccat2s1fvw  13989  swrd0  14011  swrdwrdsymb  14015  swrdspsleq  14018  reps  14123  repsw0  14130  repswccat  14139  repswrevw  14140  lswcshw  14168  cshwsexa  14177  scshwfzeqfzo  14179  lsws2  14257  lsws3  14258  lsws4  14259  wrdlen2i  14295  relexpsucnnr  14376  relexpaddg  14404  shftfib  14423  reusq0  14814  limsupcl  14822  limsupgf  14824  limsupval2  14829  isercolllem3  15015  modfsummods  15140  ackbijnn  15175  supcvg  15203  fprodfac  15319  fprodmodd  15343  fallfac0  15374  bpoly4  15405  ege2le3  15435  rpnnen2lem5  15563  ruclem11  15585  fsumdvds  15650  fproddvdsd  15676  mod2eq1n2dvds  15688  oddnn02np1  15689  oddge22np1  15690  evennn02n  15691  evennn2n  15692  bitsinv2  15782  sadaddlem  15805  smupf  15817  smup0  15818  smu01lem  15824  3lcm2e6woprm  15949  6lcm4e12  15950  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  coprmprod  15995  ge2nprmge4  16035  isprm6  16048  hashdvds  16102  phisum  16117  reumodprminv  16131  prmreclem6  16247  vdwlem13  16319  ramtlecl  16326  0ram  16346  prmdvdsprmo  16368  fvprmselgcd1  16371  prmgaplcmlem1  16377  prmgaplem7  16383  prmgaplcm  16386  cshwshashnsame  16429  prmlem0  16431  wunndx  16496  prdsval  16720  xpsbas  16837  xpsadd  16839  xpsmul  16840  xpssca  16841  xpsvsca  16842  xpsless  16843  xpsle  16844  mreexexlem2d  16908  mreacs  16921  acsfn  16922  isofn  17037  ciclcl  17064  cicrcl  17065  cicsym  17066  cicer  17068  idfu2nd  17139  idfucl  17143  fucsect  17234  initoeu2lem1  17266  initoeu2lem2  17267  setccatid  17336  setcepi  17340  catchomfval  17350  estrccatid  17374  estrreslem1  17379  estrreslem2  17380  estrres  17381  funcestrcsetclem8  17389  fullestrcsetc  17393  embedsetcestrclem  17399  funcsetcestrclem8  17404  uncfval  17476  oduglb  17741  odumeet  17742  odulub  17743  odujoin  17744  isipodrs  17763  fpwipodrs  17766  isacs5lem  17771  idmhm  17957  submacs  17983  frmdup1  18021  efmndbas  18028  sursubmefmnd  18053  injsubmefmnd  18054  idresefmnd  18056  smndex1id  18068  mgmnsgrpex  18088  mulgneg2  18253  subgacs  18305  nsgacs  18306  1nsgtrivd  18318  idrespermg  18531  psgnunilem5  18614  psgnsn  18640  odf1o2  18690  frgpuplem  18890  cntrcmnd  18955  cygctb  19005  gsumpr  19068  gsumzunsnd  19069  gsum2dlem2  19084  gsummptnn0fz  19099  dprdsubg  19139  dmdprdsplit2lem  19160  dmdprdpr  19164  dprdpr  19165  dpjeq  19174  ablfac1eulem  19187  pgpfac1lem2  19190  pgpfaclem1  19196  prmgrpsimpgd  19229  ablsimpgprmd  19230  srgbinomlem4  19286  unitgrp  19413  isirred  19445  brric  19492  subrgacs  19572  sdrgacs  19573  cntzsdrg  19574  mptscmfsupp0  19692  lssacs  19732  pwssplit1  19824  lbsextlem2  19924  lbsextlem3  19925  rlmlsm  19972  isnzr2hash  20030  0ringnnzr  20035  0ring01eqbi  20039  rng1nnzr  20040  xrsmcmn  20114  xrs1mnd  20129  xrs10  20130  gsumfsum  20158  zringlpir  20182  zringcyg  20184  zndvds  20241  regsumsupp  20311  frlmip  20467  uvcvv1  20478  lsslinds  20520  psrass1lem  20615  psrlidm  20641  resspsradd  20654  resspsrmul  20655  resspsrvsca  20656  mplcoe5lem  20707  ltbwe  20712  selvfval  20789  mhpvarcl  20798  coe1fsupp  20843  psropprmul  20867  coe1add  20893  coe1mul2lem1  20896  coe1tm  20902  cply1coe0bi  20929  evls1rhmlem  20945  evl1sca  20958  evl1var  20960  pf1mpf  20976  pf1ind  20979  matmulr  21043  ofco2  21056  mat0dimbas0  21071  mat1dimelbas  21076  mat1f1o  21083  dmatval  21097  scmatghm  21138  mavmul0  21157  mavmul0g  21158  m1detdiag  21202  mdetunilem9  21225  maducoeval2  21245  madugsum  21248  smadiadetlem0  21266  smadiadetlem1a  21268  smadiadetlem4  21274  smadiadetglem1  21276  smadiadetglem2  21277  smadiadetg  21278  cramer0  21295  cpmat  21314  mat2pmatfval  21328  cpm2mfval  21354  m2cpminvid2lem  21359  pmatcollpw3fi1lem2  21392  pmatcollpw3fi1  21393  idpm2idmp  21406  pm2mpmhmlem2  21424  chpmatfval  21435  chfacfscmulfsupp  21464  chfacfpmmulfsupp  21468  cpmidpmatlem2  21476  cpmadugsumlemF  21481  cpmidgsum2  21484  cpmadumatpolylem1  21486  cayhamlem3  21492  cayhamlem4  21493  indistopon  21606  mreclatdemoBAD  21701  mnfnei  21826  resthauslem  21968  sshauslem  21977  discmp  22003  connima  22030  1stcfb  22050  ptbasfi  22186  hauseqlcld  22251  xkoptsub  22259  xkofvcn  22289  idqtop  22311  tgqtop  22317  kqdisj  22337  xpstopnlem1  22414  xpstopnlem2  22416  ufildom1  22531  alexsubb  22651  alexsubALTlem3  22654  ptcmplem2  22658  ptcmplem3  22659  tmdgsum  22700  ustneism  22829  ustuqtop1  22847  iducn  22889  prdsmet  22977  imasdsf1olem  22980  xpsxmet  22987  xpsdsval  22988  xpsmet  22989  prdsbl  23098  met1stc  23128  prdsxmslem2  23136  xpsxms  23141  xpsms  23142  psmetutop  23174  dscmet  23179  nmoffn  23317  nmofval  23320  nmolb  23323  nmof  23325  cnbl0  23379  xrsmopn  23417  xrge0gsumle  23438  xrge0tsms  23439  negfcncf  23528  cnrehmeo  23558  lebnum  23569  xlebnum  23570  reparphti  23602  pcopt  23627  pcopt2  23628  pcorevcl  23630  pcorevlem  23631  pi1xfrval  23659  pi1xfrcnvlem  23661  pi1xfrcnv  23662  pi1cof  23664  pi1coval  23665  nmhmcn  23725  cphsubrglem  23782  csscld  23853  cmetcaulem  23892  cmpcmet  23923  csschl  23980  rrxplusgvscavalb  23999  rrxsca  24000  ehleudis  24022  divcncf  24051  ovolunlem1  24101  ovolicc2lem4  24124  ioovolcl  24174  ioorcl2  24176  uniioovol  24183  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  dyadmbllem  24203  mbfsub  24266  itg1climres  24318  xrge0f  24335  itg2ge0  24339  itg20  24341  itg2monolem1  24354  itg2i1fseq2  24360  ibl0  24390  ellimc2  24480  limcflf  24484  dvreslem  24512  dvidlem  24518  dvmptresicc  24519  dvid  24521  cpnres  24540  dvaddbr  24541  dvmulbr  24542  dvfre  24554  dvexp  24556  dvrec  24558  dvmptid  24560  dvmptc  24561  dvmptntr  24574  dvexp3  24581  dvlipcn  24597  dveq0  24603  dv11cn  24604  lhop2  24618  ftc1a  24640  itgpowd  24653  tdeglem1  24659  tdeglem3  24660  tdeglem4  24661  tdeglem2  24662  mdeg0  24671  mdegle0  24678  ply1remlem  24763  plypf1  24809  coe0  24853  dvply1  24880  elqaalem3  24917  aaliou2b  24937  aaliou3lem8  24941  aaliou3lem7  24945  taylfvallem  24953  taylf  24956  tayl0  24957  taylpfval  24960  taylply  24964  dvtaylp  24965  taylthlem1  24968  taylthlem2  24969  ulmdvlem1  24995  ulmdvlem2  24996  ulmdvlem3  24997  radcnvcl  25012  psercnlem2  25019  psercn  25021  pserdv  25024  abelthlem3  25028  abelth  25036  sincn  25039  coscn  25040  reefgim  25045  tangtx  25098  pige3ALT  25112  cos02pilt1  25118  cosordlem  25122  logcn  25238  dvlog  25242  advlog  25245  advlogexp  25246  logtayl  25251  logccv  25254  dvcxp1  25329  dvcncxp1  25332  cxpcn3lem  25336  cxpcn3  25337  resqrtcn  25338  sqrtcn  25339  loglesqrt  25347  logbfval  25376  isosctrlem2  25405  dquartlem1  25437  quart  25447  atancj  25496  efiatan  25498  atantan  25509  atanbndlem  25511  atansopn  25518  dvatan  25521  atantayl  25523  leibpilem2  25527  leibpi  25528  log2tlbnd  25531  rlimcnp2  25552  efrlim  25555  divsqrtsumlem  25565  jensenlem1  25572  jensenlem2  25573  jensen  25574  amgmlem  25575  amgm  25576  emcllem4  25584  emcllem7  25587  lgamcvg2  25640  gamcvg2lem  25644  wilthlem2  25654  wilthlem3  25655  basellem6  25671  chtrpcl  25760  ppiltx  25762  1sgm2ppw  25784  chtlepsi  25790  chpub  25804  logfacbnd3  25807  logfacrlim  25808  perfectlem2  25814  dchrelbas2  25821  dchrabs  25844  dchrhash  25855  bposlem7  25874  lgsdir2lem5  25913  lgsqrlem1  25930  gausslemma2dlem5  25955  gausslemma2dlem6  25956  lgseisenlem4  25962  lgsquad2lem1  25968  lgsquad3  25971  2sqreu  26040  2sqreunn  26041  2sqreult  26042  2sqreultb  26043  2sqreunnlt  26044  chpo1ub  26064  vmadivsumb  26067  rpvmasumlem  26071  dchrisumlem2  26074  dchrmusumlema  26077  dchrvmasumlem2  26082  dchrvmasumlema  26084  dchrvmasumiflem1  26085  dchrisum0flblem1  26092  dchrisum0lem1  26100  rplogsum  26111  mudivsum  26114  logdivsum  26117  mulog2sumlem2  26119  vmalogdivsum2  26122  2vmadivsumlem  26124  log2sumbnd  26128  selberglem2  26130  selbergb  26133  selberg2lem  26134  selberg2b  26136  selberg3lem1  26141  selberg4lem1  26144  selberg4  26145  pntrsumo1  26149  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntibndlem1  26173  pntibndlem2  26175  pntibndlem3  26176  pntlemb  26181  pntlemr  26186  pntlemf  26189  pntlem3  26193  pnt  26198  qabvle  26209  padicabv  26214  ostth1  26217  istrkg2ld  26254  tgldimor  26296  motgrp  26337  perpln1  26504  perpln2  26505  isperp  26506  snstrvtxval  26830  snstriedgval  26831  isuhgrop  26863  uhgrunop  26868  uhgrstrrepe  26871  upgrop  26887  upgrunop  26912  umgrunop  26914  isusgrs  26949  isuspgrop  26954  isusgrop  26955  usgrop  26956  usgrstrrepe  27025  uspgr1ewop  27038  usgr2v1e2w  27042  uhgrspan1  27093  upgrres  27096  umgrres  27097  usgrres  27098  upgrres1  27103  umgrres1  27104  usgrres1  27105  isfusgrcl  27111  fusgredgfi  27115  usgr1v0e  27116  nbgrval  27126  nbusgrf1o1  27160  nbfusgrlevtxm2  27168  uvtx01vtx  27187  usgrexilem  27230  usgrexi  27231  cusgrexi  27233  structtousgr  27235  structtocusgr  27236  cusgrres  27238  cusgrfilem3  27247  sizusglecusg  27253  vtxdgfval  27257  vtxdgop  27260  vtxdgf  27261  vtxdlfgrval  27275  vtxd0nedgb  27278  vtxdusgr0edgnelALT  27286  1loopgrvd0  27294  1egrvtxdg1  27299  1egrvtxdg0  27301  p1evtxdeqlem  27302  p1evtxdeq  27303  p1evtxdp1  27304  umgr2v2e  27315  vdiscusgrb  27320  vdegp1ai  27326  vdegp1bi  27327  ewlkle  27395  wksfval  27399  wksv  27409  wlk1ewlk  27429  uspgr2wlkeq  27435  wlkp1lem8  27470  upgr2pthnlp  27521  wlkiswwlks2  27661  wlksnwwlknvbij  27694  2pthdlem1  27716  wpthswwlks2on  27747  elwwlks2  27752  elwspths2spth  27753  clwlkclwwlklem1  27784  clwwlknfi  27830  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  clwwlkvbij  27898  0wlkonlem1  27903  0wlkons1  27906  0pthon  27912  3wlkdlem4  27947  upgr3v3e3cycl  27965  trlsegvdeglem3  28007  trlsegvdeglem5  28009  eupth2lemb  28022  frgr3v  28060  frgr2wwlk1  28114  fusgreghash2wspv  28120  ex-lcm  28243  vsfval  28416  ipasslem7  28619  minvecolem2  28658  h2hcau  28762  h2hlm  28763  hlimadd  28976  hhsscms  29061  chocunii  29084  occllem  29086  eigposi  29619  leopnmid  29921  opsqrlem1  29923  hmopidmchi  29934  mdslj1i  30102  addltmulALT  30229  imadifxp  30364  2ndimaxp  30409  2ndresdju  30411  fressupp  30448  fsuppcurry1  30487  fsuppcurry2  30488  xaddeq0  30503  fzodif2  30541  pwrssmgc  30706  xrge0npcan  30728  gsumpart  30740  gsumhashmul  30741  xrge0tsmsd  30742  gsumle  30775  symgcom  30777  cycpmfvlem  30804  cycpmfv3  30807  cycpmconjslem2  30847  islinds5  30983  ellspds  30984  locfinreflem  31193  locfinref  31194  zarcmplem  31234  xpinpreima2  31260  cnre2csqlem  31263  tpr2rico  31265  ordtrestNEW  31274  ordtrest2NEW  31276  mndpluscn  31279  pnfneige0  31304  qqhghm  31339  qqhrhm  31340  qqhcn  31342  qqhucn  31343  rrhcn  31348  rrhre  31372  esumsplit  31422  esumpr  31435  esumfsup  31439  sigaclcu2  31489  pwsiga  31499  prsiga  31500  sigapildsys  31531  ldgenpisyslem1  31532  measvuni  31583  elmbfmvol2  31635  mbfmcnt  31636  sxbrsigalem1  31653  sxbrsiga  31658  omsfval  31662  carsgclctunlem2  31687  sibf0  31702  sitgclg  31710  sitmval  31717  eulerpartgbij  31740  eulerpartlemgh  31746  isrrvv  31811  rrvadd  31820  rrvmulc  31821  dstrvprob  31839  coinflipspace  31848  coinfliprv  31850  ballotlemfmpn  31862  ballotlem1ri  31902  sgnmulsgn  31917  plymul02  31926  signsplypnf  31930  signsply0  31931  signswrid  31938  prodfzo03  31984  itgexpif  31987  circlemethhgt  32024  hgt750lemb  32037  cardpred  32473  indispconn  32594  connpconn  32595  iccllysconn  32610  cvmopnlem  32638  cvmliftlem15  32658  cvmlift2lem3  32665  satfn  32715  satom  32716  satfv0  32718  ex-sategoelelomsuc  32786  prv0  32790  prv1n  32791  mrsubff  32872  mrsubccat  32878  circum  33030  noextend  33286  nosupbnd2lem1  33328  elhf2  33749  bj-elid4  34583  bj-endbase  34730  bj-endcomp  34731  irrdifflemf  34739  topdifinfindis  34763  icoreelrn  34778  finxpreclem2  34807  finixpnum  35042  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem5  35062  poimirlem10  35067  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  dvtan  35107  itg2addnclem  35108  ftc1anclem5  35134  dvasin  35141  dvreasin  35143  dvreacos  35144  areacirclem1  35145  areacirc  35150  bnd2lem  35229  prdsbnd  35231  cntotbnd  35234  cnpwstotbnd  35235  isdrngo2  35396  prter2  36177  eqlkr2  36396  tendoidcl  38065  cdlemk56  38267  dihpN  38632  mapdhval  39020  hlhillcs  39254  lcmineqlem9  39325  frlmvscadiccat  39440  fsuppind  39456  fsuppssind  39459  nn0rppwr  39490  sn-00idlem3  39538  remul02  39543  remul01  39545  reixi  39559  remulid2  39570  sn-0tie0  39576  mulgt0b2d  39585  prjspreln0  39603  3cubes  39631  isnacs3  39651  diophrw  39700  lzenom  39711  diophin  39713  pellexlem5  39774  pw2f1ocnv  39978  dnnumch2  39989  kelac2lem  40008  kelac2  40009  dfac21  40010  pwfi2f1o  40040  frlmpwfi  40042  mpaaeu  40094  rngunsnply  40117  mendbas  40128  mendplusgfval  40129  mendmulrfval  40131  mendsca  40133  mendvscafval  40134  idomodle  40140  proot1ex  40145  deg1mhm  40151  alephiso2  40257  trclubgNEW  40318  dmtrcl  40327  rntrcl  40328  brfvidRP  40389  trclrelexplem  40412  relexp01min  40414  trclimalb2  40427  dssmapfvd  40718  ntrk0kbimka  40742  ntrrn  40825  dssmapntrcls  40831  amgm2d  40904  amgm3d  40905  amgm4d  40906  hashnzfzclim  41026  ofsubid  41028  ofdivrec  41030  dvconstbi  41038  wessf1ornlem  41811  fzisoeu  41932  iuneqfzuzlem  41966  sumnnodd  42272  limsuppnfdlem  42343  liminfgf  42400  negcncfg  42523  cnfdmsn  42524  itgcoscmulx  42611  stoweidlem13  42655  stoweidlem26  42668  stoweidlem34  42676  stoweidlem42  42684  stoweidlem44  42686  stoweidlem48  42690  stoweidlem62  42704  stoweid  42705  stirlinglem7  42722  stirlinglem11  42726  stirlinglem12  42727  dirkeritg  42744  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem24  42773  fourierdlem48  42796  fourierdlem49  42797  fourierdlem62  42810  fourierdlem70  42818  fourierdlem80  42828  fourierdlem83  42831  fourierdlem85  42833  fourierdlem102  42850  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem114  42862  etransclem18  42894  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem35  42911  etransclem46  42922  prsal  42960  ovolval5lem3  43293  setsidel  43893  fundcmpsurbijinjpreimafv  43924  iccpartipre  43938  iccpartiltu  43939  sprval  43996  sprbisymrel  44016  prprval  44031  prprelprb  44034  fmtnoprmfac2lem1  44083  mod42tp1mod8  44120  sfprmdvdsmersenne  44121  perfectALTVlem2  44240  fpprel2  44259  stgoldbwt  44294  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  isomuspgrlem2  44351  ushrisomgr  44359  upwlksfval  44363  uspgrbisymrelALT  44383  idmgmhm  44408  mgmplusgiopALT  44454  sgrp2sgrp  44488  isrnghm  44516  lidlmmgm  44549  zlidlring  44552  2zrngnmlid  44573  dfrngc2  44596  rnghmsscmap2  44597  rnghmsscmap  44598  rngchomfvalALTV  44608  rngcidALTV  44615  funcrngcsetcALT  44623  dfringc2  44642  rhmsscmap2  44643  rhmsscmap  44644  rhmsscrnghm  44650  rngcresringcat  44654  funcringcsetcALTV2lem8  44667  ringchomfvalALTV  44671  ringcidALTV  44678  funcringcsetclem8ALTV  44690  srhmsubc  44700  fldc  44707  rngcrescrhm  44709  rhmsubclem3  44712  srhmsubcALTV  44718  fldcALTV  44725  rngcrescrhmALTV  44727  altgsumbcALT  44755  zlmodzxzel  44757  zlmodzxzsubm  44761  zlmodzxzsub  44762  scmsuppss  44774  ply1mulgsum  44798  dmatALTbas  44810  lcoop  44820  lincval0  44824  lco0  44836  linds0  44874  snlindsntorlem  44879  lmod1lem2  44897  lmod1lem3  44898  lmod1zr  44902  lmod1zrnlvec  44903  zlmodzxznm  44906  zlmodzxzldeplem4  44912  expnegico01  44927  pw2m1lepw2m1  44929  fldivexpfllog2  44979  blennnelnn  44990  blenpw2  44992  nnpw2pmod  44997  blennnt2  45003  nnolog2flm1  45004  digfval  45011  dignnld  45017  dig2nn0ld  45018  0dig2nn0e  45026  0dig2nn0o  45027  1arymaptf1  45056  2arymaptf1  45067  itcovalendof  45083  itcovalt2lem1  45089  rrx2plordisom  45137  ehl2eudisval0  45139  rrxlines  45147  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrxsphere  45162  line2  45166  line2x  45168  line2y  45169  inlinecirc02preu  45202  amgmwlem  45330  amgmlemALT  45331  amgmw2d  45332