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  5676  poirr2  5984  fvrnressn  6923  isomin  7090  isoini  7091  mptmpoopabbrd  7778  supp0  7835  suppval1  7836  suppssr  7861  dmtpos  7904  mpocurryd  7935  oaabs2  8272  elqsecl  8351  mapsncnv  8457  boxcutc  8505  domunsncan  8617  unxpdom2  8726  sucxpdom  8727  findcard2d  8760  ac6sfi  8762  xpfi  8789  imafi  8817  snopfsupp  8856  fifo  8896  ordtypelem4  8985  oismo  9004  wofib  9009  brwdom2  9037  canthwdom  9043  cantnfval  9131  cantnflt  9135  cantnff  9137  cantnf0  9138  cantnflem1b  9149  cantnflem1  9152  cnfcom  9163  cnfcom2lem  9164  ranksnb  9256  updjudhcoinlf  9361  updjudhcoinrg  9362  updjud  9363  tskwe  9379  cardidm  9388  infxpenc  9444  fseqdom  9452  dfac8clem  9458  dfac12lem2  9570  infmap2  9640  fin23lem14  9755  fin23lem40  9773  isf34lem7  9801  isf34lem6  9802  fin1a2lem12  9833  hsmexlem4  9851  hsmexlem5  9852  ac5b  9900  alephexp1  10001  alephsuc3  10002  fpwwe2lem8  10059  fpwwe2lem13  10064  canthwe  10073  canthp1lem2  10075  gchdju1  10078  pwfseqlem5  10085  wunco  10155  prlem934  10455  supsrlem  10533  msqge0  11161  negfi  11589  ofnegsub  11636  ofsubge0  11637  xaddpnf1  12620  supxrmnf  12711  fz0sn0fz1  13025  injresinjlem  13158  fldiv4lem1div2  13208  uzindi  13351  seqfeq4  13420  seqof  13428  bcval5  13679  hashdomi  13742  hash1snb  13781  hashmap  13797  hashge2el2difr  13840  hashtpg  13844  fi1uzind  13856  ccatlen  13927  ccatlenOLD  13928  ccat0  13929  lswccatn0lsw  13945  ccatalpha  13947  s111  13969  ccat2s1fvw  13998  swrd0  14020  swrdwrdsymb  14024  swrdspsleq  14027  reps  14132  repsw0  14139  repswccat  14148  repswrevw  14149  lswcshw  14177  cshwsexa  14186  scshwfzeqfzo  14188  lsws2  14266  lsws3  14267  lsws4  14268  wrdlen2i  14304  relexpsucnnr  14384  relexpaddg  14412  shftfib  14431  reusq0  14822  limsupcl  14830  limsupgf  14832  limsupval2  14837  isercolllem3  15023  modfsummods  15148  ackbijnn  15183  supcvg  15211  fprodfac  15327  fprodmodd  15351  fallfac0  15382  bpoly4  15413  ege2le3  15443  rpnnen2lem5  15571  ruclem11  15593  fsumdvds  15658  fproddvdsd  15684  mod2eq1n2dvds  15696  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  bitsinv2  15792  sadaddlem  15815  smupf  15827  smup0  15828  smu01lem  15834  3lcm2e6woprm  15959  6lcm4e12  15960  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  coprmprod  16005  ge2nprmge4  16045  isprm6  16058  hashdvds  16112  phisum  16127  reumodprminv  16141  prmreclem6  16257  vdwlem13  16329  ramtlecl  16336  0ram  16356  prmdvdsprmo  16378  fvprmselgcd1  16381  prmgaplcmlem1  16387  prmgaplem7  16393  prmgaplcm  16396  cshwshashnsame  16437  prmlem0  16439  wunndx  16504  prdsval  16728  xpsbas  16845  xpsadd  16847  xpsmul  16848  xpssca  16849  xpsvsca  16850  xpsless  16851  xpsle  16852  mreexexlem2d  16916  mreacs  16929  acsfn  16930  isofn  17045  ciclcl  17072  cicrcl  17073  cicsym  17074  cicer  17076  idfu2nd  17147  idfucl  17151  fucsect  17242  initoeu2lem1  17274  initoeu2lem2  17275  setccatid  17344  setcepi  17348  catchomfval  17358  estrccatid  17382  estrreslem1  17387  estrreslem2  17388  estrres  17389  funcestrcsetclem8  17397  fullestrcsetc  17401  embedsetcestrclem  17407  funcsetcestrclem8  17412  uncfval  17484  oduglb  17749  odumeet  17750  odulub  17751  odujoin  17752  isipodrs  17771  fpwipodrs  17774  isacs5lem  17779  idmhm  17965  submacs  17991  frmdup1  18029  efmndbas  18036  sursubmefmnd  18061  injsubmefmnd  18062  idresefmnd  18064  smndex1id  18076  mgmnsgrpex  18096  mulgneg2  18261  subgacs  18313  nsgacs  18314  1nsgtrivd  18326  idrespermg  18539  psgnunilem5  18622  psgnsn  18648  odf1o2  18698  frgpuplem  18898  cntrcmnd  18962  cygctb  19012  gsumpr  19075  gsumzunsnd  19076  gsum2dlem2  19091  gsummptnn0fz  19106  dprdsubg  19146  dmdprdsplit2lem  19167  dmdprdpr  19171  dprdpr  19172  dpjeq  19181  ablfac1eulem  19194  pgpfac1lem2  19197  pgpfaclem1  19203  prmgrpsimpgd  19236  ablsimpgprmd  19237  srgbinomlem4  19293  unitgrp  19417  isirred  19449  brric  19499  subrgacs  19579  sdrgacs  19580  cntzsdrg  19581  mptscmfsupp0  19699  lssacs  19739  pwssplit1  19831  lbsextlem2  19931  lbsextlem3  19932  rlmlsm  19979  isnzr2hash  20037  0ringnnzr  20042  0ring01eqbi  20046  rng1nnzr  20047  psrass1lem  20157  psrlidm  20183  resspsradd  20196  resspsrmul  20197  resspsrvsca  20198  mplcoe5lem  20248  ltbwe  20253  selvfval  20330  coe1fsupp  20382  psropprmul  20406  coe1add  20432  coe1mul2lem1  20435  coe1tm  20441  cply1coe0bi  20468  evls1rhmlem  20484  evl1sca  20497  evl1var  20499  pf1mpf  20515  pf1ind  20518  xrsmcmn  20568  xrs1mnd  20583  xrs10  20584  gsumfsum  20612  zringlpir  20636  zringcyg  20638  zndvds  20696  regsumsupp  20766  frlmip  20922  uvcvv1  20933  lsslinds  20975  matmulr  21047  ofco2  21060  mat0dimbas0  21075  mat1dimelbas  21080  mat1f1o  21087  dmatval  21101  scmatghm  21142  mavmul0  21161  mavmul0g  21162  m1detdiag  21206  mdetunilem9  21229  maducoeval2  21249  madugsum  21252  smadiadetlem0  21270  smadiadetlem1a  21272  smadiadetlem4  21278  smadiadetglem1  21280  smadiadetglem2  21281  smadiadetg  21282  cramer0  21299  cpmat  21317  mat2pmatfval  21331  cpm2mfval  21357  m2cpminvid2lem  21362  pmatcollpw3fi1lem2  21395  pmatcollpw3fi1  21396  idpm2idmp  21409  pm2mpmhmlem2  21427  chpmatfval  21438  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  cpmidpmatlem2  21479  cpmadugsumlemF  21484  cpmidgsum2  21487  cpmadumatpolylem1  21489  cayhamlem3  21495  cayhamlem4  21496  indistopon  21609  mreclatdemoBAD  21704  mnfnei  21829  resthauslem  21971  sshauslem  21980  discmp  22006  connima  22033  1stcfb  22053  ptbasfi  22189  hauseqlcld  22254  xkoptsub  22262  xkofvcn  22292  idqtop  22314  tgqtop  22320  kqdisj  22340  xpstopnlem1  22417  xpstopnlem2  22419  ufildom1  22534  alexsubb  22654  alexsubALTlem3  22657  ptcmplem2  22661  ptcmplem3  22662  tmdgsum  22703  ustneism  22832  ustuqtop1  22850  iducn  22892  prdsmet  22980  imasdsf1olem  22983  xpsxmet  22990  xpsdsval  22991  xpsmet  22992  prdsbl  23101  met1stc  23131  prdsxmslem2  23139  xpsxms  23144  xpsms  23145  psmetutop  23177  dscmet  23182  nmoffn  23320  nmofval  23323  nmolb  23326  nmof  23328  cnbl0  23382  xrsmopn  23420  xrge0gsumle  23441  xrge0tsms  23442  negfcncf  23527  cnrehmeo  23557  lebnum  23568  xlebnum  23569  reparphti  23601  pcopt  23626  pcopt2  23627  pcorevcl  23629  pcorevlem  23630  pi1xfrval  23658  pi1xfrcnvlem  23660  pi1xfrcnv  23661  pi1cof  23663  pi1coval  23664  nmhmcn  23724  cphsubrglem  23781  csscld  23852  cmetcaulem  23891  cmpcmet  23922  csschl  23979  rrxplusgvscavalb  23998  rrxsca  23999  ehleudis  24021  divcncf  24048  ovolunlem1  24098  ovolicc2lem4  24121  ioovolcl  24171  ioorcl2  24173  uniioovol  24180  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  dyadmbllem  24200  mbfsub  24263  itg1climres  24315  xrge0f  24332  itg2ge0  24336  itg20  24338  itg2monolem1  24351  itg2i1fseq2  24357  ibl0  24387  ellimc2  24475  limcflf  24479  dvreslem  24507  dvidlem  24513  dvid  24515  cpnres  24534  dvaddbr  24535  dvmulbr  24536  dvfre  24548  dvexp  24550  dvrec  24552  dvmptid  24554  dvmptc  24555  dvmptntr  24568  dvexp3  24575  dvlipcn  24591  dveq0  24597  dv11cn  24598  lhop2  24612  ftc1a  24634  tdeglem1  24652  tdeglem3  24653  tdeglem4  24654  tdeglem2  24655  mdeg0  24664  mdegle0  24671  ply1remlem  24756  plypf1  24802  coe0  24846  dvply1  24873  elqaalem3  24910  aaliou2b  24930  aaliou3lem8  24934  aaliou3lem7  24938  taylfvallem  24946  taylf  24949  tayl0  24950  taylpfval  24953  taylply  24957  dvtaylp  24958  taylthlem1  24961  taylthlem2  24962  ulmdvlem1  24988  ulmdvlem2  24989  ulmdvlem3  24990  radcnvcl  25005  psercnlem2  25012  psercn  25014  pserdv  25017  abelthlem3  25021  abelth  25029  sincn  25032  coscn  25033  reefgim  25038  tangtx  25091  pige3ALT  25105  cos02pilt1  25111  cosordlem  25115  logcn  25230  dvlog  25234  advlog  25237  advlogexp  25238  logtayl  25243  logccv  25246  dvcxp1  25321  dvcncxp1  25324  cxpcn3lem  25328  cxpcn3  25329  resqrtcn  25330  sqrtcn  25331  loglesqrt  25339  logbfval  25368  isosctrlem2  25397  dquartlem1  25429  quart  25439  atancj  25488  efiatan  25490  atantan  25501  atanbndlem  25503  atansopn  25510  dvatan  25513  atantayl  25515  leibpilem2  25519  leibpi  25520  log2tlbnd  25523  rlimcnp2  25544  efrlim  25547  divsqrtsumlem  25557  jensenlem1  25564  jensenlem2  25565  jensen  25566  amgmlem  25567  amgm  25568  emcllem4  25576  emcllem7  25579  lgamcvg2  25632  gamcvg2lem  25636  wilthlem2  25646  wilthlem3  25647  basellem6  25663  chtrpcl  25752  ppiltx  25754  1sgm2ppw  25776  chtlepsi  25782  chpub  25796  logfacbnd3  25799  logfacrlim  25800  perfectlem2  25806  dchrelbas2  25813  dchrabs  25836  dchrhash  25847  bposlem7  25866  lgsdir2lem5  25905  lgsqrlem1  25922  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgseisenlem4  25954  lgsquad2lem1  25960  lgsquad3  25963  2sqreu  26032  2sqreunn  26033  2sqreult  26034  2sqreultb  26035  2sqreunnlt  26036  chpo1ub  26056  vmadivsumb  26059  rpvmasumlem  26063  dchrisumlem2  26066  dchrmusumlema  26069  dchrvmasumlem2  26074  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0lem1  26092  rplogsum  26103  mudivsum  26106  logdivsum  26109  mulog2sumlem2  26111  vmalogdivsum2  26114  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selbergb  26125  selberg2lem  26126  selberg2b  26128  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntibndlem1  26165  pntibndlem2  26167  pntibndlem3  26168  pntlemb  26173  pntlemr  26178  pntlemf  26181  pntlem3  26185  pnt  26190  qabvle  26201  padicabv  26206  ostth1  26209  istrkg2ld  26246  tgldimor  26288  motgrp  26329  perpln1  26496  perpln2  26497  isperp  26498  snstrvtxval  26822  snstriedgval  26823  isuhgrop  26855  uhgrunop  26860  uhgrstrrepe  26863  upgrop  26879  upgrunop  26904  umgrunop  26906  isusgrs  26941  isuspgrop  26946  isusgrop  26947  usgrop  26948  usgrstrrepe  27017  uspgr1ewop  27030  usgr2v1e2w  27034  uhgrspan1  27085  upgrres  27088  umgrres  27089  usgrres  27090  upgrres1  27095  umgrres1  27096  usgrres1  27097  isfusgrcl  27103  fusgredgfi  27107  usgr1v0e  27108  nbgrval  27118  nbusgrf1o1  27152  nbfusgrlevtxm2  27160  uvtx01vtx  27179  usgrexilem  27222  usgrexi  27223  cusgrexi  27225  structtousgr  27227  structtocusgr  27228  cusgrres  27230  cusgrfilem3  27239  sizusglecusg  27245  vtxdgfval  27249  vtxdgop  27252  vtxdgf  27253  vtxdlfgrval  27267  vtxd0nedgb  27270  vtxdusgr0edgnelALT  27278  1loopgrvd0  27286  1egrvtxdg1  27291  1egrvtxdg0  27293  p1evtxdeqlem  27294  p1evtxdeq  27295  p1evtxdp1  27296  umgr2v2e  27307  vdiscusgrb  27312  vdegp1ai  27318  vdegp1bi  27319  ewlkle  27387  wksfval  27391  wksv  27401  wlk1ewlk  27421  uspgr2wlkeq  27427  wlkp1lem8  27462  upgr2pthnlp  27513  wlkiswwlks2  27653  wlksnwwlknvbij  27687  2pthdlem1  27709  wpthswwlks2on  27740  elwwlks2  27745  elwspths2spth  27746  clwlkclwwlklem1  27777  clwwlknfi  27823  clwwlknfiOLD  27824  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlkvbij  27892  0wlkonlem1  27897  0wlkons1  27900  0pthon  27906  3wlkdlem4  27941  upgr3v3e3cycl  27959  trlsegvdeglem3  28001  trlsegvdeglem5  28003  eupth2lemb  28016  frgr3v  28054  frgr2wwlk1  28108  fusgreghash2wspv  28114  ex-lcm  28237  vsfval  28410  ipasslem7  28613  minvecolem2  28652  h2hcau  28756  h2hlm  28757  hlimadd  28970  hhsscms  29055  chocunii  29078  occllem  29080  eigposi  29613  leopnmid  29915  opsqrlem1  29917  hmopidmchi  29928  mdslj1i  30096  addltmulALT  30223  imadifxp  30351  fsuppcurry1  30461  fsuppcurry2  30462  xaddeq0  30477  fzodif2  30515  xrge0npcan  30681  xrge0tsmsd  30692  gsumle  30725  symgcom  30727  cycpmfvlem  30754  cycpmfv3  30757  cycpmconjslem2  30797  islinds5  30932  ellspds  30933  locfinreflem  31104  locfinref  31105  xpinpreima2  31150  cnre2csqlem  31153  tpr2rico  31155  ordtrestNEW  31164  ordtrest2NEW  31166  mndpluscn  31169  pnfneige0  31194  qqhghm  31229  qqhrhm  31230  qqhcn  31232  qqhucn  31233  rrhcn  31238  rrhre  31262  esumsplit  31312  esumpr  31325  esumfsup  31329  sigaclcu2  31379  pwsiga  31389  prsiga  31390  sigapildsys  31421  ldgenpisyslem1  31422  measvuni  31473  elmbfmvol2  31525  mbfmcnt  31526  sxbrsigalem1  31543  sxbrsiga  31548  omsfval  31552  carsgclctunlem2  31577  sibf0  31592  sitgclg  31600  sitmval  31607  eulerpartgbij  31630  eulerpartlemgh  31636  isrrvv  31701  rrvadd  31710  rrvmulc  31711  dstrvprob  31729  coinflipspace  31738  coinfliprv  31740  ballotlemfmpn  31752  ballotlem1ri  31792  sgnmulsgn  31807  plymul02  31816  signsplypnf  31820  signsply0  31821  signswrid  31828  prodfzo03  31874  itgexpif  31877  circlemethhgt  31914  hgt750lemb  31927  indispconn  32481  connpconn  32482  iccllysconn  32497  cvmopnlem  32525  cvmliftlem15  32545  cvmlift2lem3  32552  satfn  32602  satom  32603  satfv0  32605  ex-sategoelelomsuc  32673  prv0  32677  prv1n  32678  mrsubff  32759  mrsubccat  32765  circum  32917  noextend  33173  nosupbnd2lem1  33215  elhf2  33636  bj-elid4  34463  bj-endbase  34600  bj-endcomp  34601  topdifinfindis  34630  icoreelrn  34645  finxpreclem2  34674  finixpnum  34892  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem5  34912  poimirlem10  34917  poimirlem22  34929  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  dvtan  34957  itg2addnclem  34958  ftc1anclem5  34986  dvasin  34993  dvreasin  34995  dvreacos  34996  areacirclem1  34997  areacirc  35002  bnd2lem  35084  prdsbnd  35086  cntotbnd  35089  cnpwstotbnd  35090  isdrngo2  35251  prter2  36032  eqlkr2  36251  tendoidcl  37920  cdlemk56  38122  dihpN  38487  mapdhval  38875  hlhillcs  39109  frlmvscadiccat  39194  nn0rppwr  39231  sn-00idlem3  39279  remul02  39284  remul01  39286  remulid2  39298  prjspreln0  39308  3cubes  39336  isnacs3  39356  diophrw  39405  lzenom  39416  diophin  39418  pellexlem5  39479  pw2f1ocnv  39683  dnnumch2  39694  kelac2lem  39713  kelac2  39714  dfac21  39715  pwfi2f1o  39745  frlmpwfi  39747  mpaaeu  39799  rngunsnply  39822  mendbas  39833  mendplusgfval  39834  mendmulrfval  39836  mendsca  39838  mendvscafval  39839  idomodle  39845  proot1ex  39850  deg1mhm  39856  itgpowd  39870  alephiso2  39966  trclubgNEW  40027  dmtrcl  40036  rntrcl  40037  brfvidRP  40082  trclrelexplem  40105  relexp01min  40107  trclimalb2  40120  dssmapfvd  40412  ntrk0kbimka  40438  ntrrn  40521  dssmapntrcls  40527  amgm2d  40600  amgm3d  40601  amgm4d  40602  hashnzfzclim  40703  ofsubid  40705  ofdivrec  40707  dvconstbi  40715  wessf1ornlem  41494  fzisoeu  41616  iuneqfzuzlem  41651  sumnnodd  41960  limsuppnfdlem  42031  liminfgf  42088  negcncfg  42213  cnfdmsn  42214  dvmptresicc  42253  itgcoscmulx  42303  stoweidlem13  42347  stoweidlem26  42360  stoweidlem34  42368  stoweidlem42  42376  stoweidlem44  42378  stoweidlem48  42382  stoweidlem62  42396  stoweid  42397  stirlinglem7  42414  stirlinglem11  42418  stirlinglem12  42419  dirkeritg  42436  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem24  42465  fourierdlem48  42488  fourierdlem49  42489  fourierdlem62  42502  fourierdlem70  42510  fourierdlem80  42520  fourierdlem83  42523  fourierdlem85  42525  fourierdlem102  42542  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem114  42554  etransclem18  42586  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem35  42603  etransclem46  42614  prsal  42652  ovolval5lem3  42985  setsidel  43585  fundcmpsurbijinjpreimafv  43616  iccpartipre  43630  iccpartiltu  43631  sprval  43690  sprbisymrel  43710  prprval  43725  prprelprb  43728  fmtnoprmfac2lem1  43777  mod42tp1mod8  43816  sfprmdvdsmersenne  43817  perfectALTVlem2  43936  fpprel2  43955  stgoldbwt  43990  nnsum3primesgbe  44006  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem2  44020  isomuspgrlem2  44047  ushrisomgr  44055  upwlksfval  44059  uspgrbisymrelALT  44079  idmgmhm  44104  mgmplusgiopALT  44150  sgrp2sgrp  44184  isrnghm  44212  lidlmmgm  44245  zlidlring  44248  2zrngnmlid  44269  dfrngc2  44292  rnghmsscmap2  44293  rnghmsscmap  44294  rngchomfvalALTV  44304  rngcidALTV  44311  funcrngcsetcALT  44319  dfringc2  44338  rhmsscmap2  44339  rhmsscmap  44340  rhmsscrnghm  44346  rngcresringcat  44350  funcringcsetcALTV2lem8  44363  ringchomfvalALTV  44367  ringcidALTV  44374  funcringcsetclem8ALTV  44386  srhmsubc  44396  fldc  44403  rngcrescrhm  44405  rhmsubclem3  44408  srhmsubcALTV  44414  fldcALTV  44421  rngcrescrhmALTV  44423  altgsumbcALT  44450  zlmodzxzel  44452  zlmodzxzsubm  44456  zlmodzxzsub  44457  scmsuppss  44469  ply1mulgsum  44493  dmatALTbas  44505  lcoop  44515  lincval0  44519  lco0  44531  linds0  44569  snlindsntorlem  44574  lmod1lem2  44592  lmod1lem3  44593  lmod1zr  44597  lmod1zrnlvec  44598  zlmodzxznm  44601  zlmodzxzldeplem4  44607  expnegico01  44622  pw2m1lepw2m1  44624  fldivexpfllog2  44674  blennnelnn  44685  blenpw2  44687  nnpw2pmod  44692  blennnt2  44698  nnolog2flm1  44699  digfval  44706  dignnld  44712  dig2nn0ld  44713  0dig2nn0e  44721  0dig2nn0o  44722  rrx2plordisom  44759  ehl2eudisval0  44761  rrxlines  44769  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrxsphere  44784  line2  44788  line2x  44790  line2y  44791  inlinecirc02preu  44824  amgmwlem  44952  amgmlemALT  44953  amgmw2d  44954