Theorem mpan2 704

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	⊢ 𝜓
mpan2.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpan2	⊢ (𝜑 → 𝜒)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpan2.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpdan 700	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanr12  718  mp3an23  1483  elvd  3460  elabg  3633  eueq2  3671  sbcgf  3812  sbcralg  3825  csbconstgf  3869  sbcnestgw  4384  csbnestgw  4385  sbcnestg  4389  csbnestg  4390  csbnest1g  4393  ssex  5289  iinexg  5316  eusv2nf  5364  reusv2lem5  5371  nnullss  5437  xpss1  5677  xpiindi  5822  reldm0  5922  elrnmpt1s  5953  resdm  6033  eliniseg  6110  trinxp  6137  ssrnres  6188  cnveq0  6209  coi2  6286  relrelss  6299  relresfld  6302  cnviin  6313  elpred  6347  onelssex  6438  ord0eln0  6445  funcnvres  6648  funimaex  6657  fnresin1  6694  fnresin2  6695  fresin  6781  ssimaex  7001  fvmpt  7024  fvmptnf  7047  fvimacnvALT  7087  dff3  7132  fsn  7168  fsn2  7169  funop  7185  fvrnressn  7197  fnsnbg  7201  fninfp  7210  fndifnfp  7212  fnnfpeq0  7214  fprb  7230  elabrex  7277  elabrexg  7278  f1elima  7298  f1ofvswap  7345  fliftel1  7349  f1owe  7392  f1oweOLD  7393  sorpssuni  7780  sorpssint  7781  eldifpw  7814  ordeleqon  7830  ordsson  7831  ssnlim  7931  abrexexg  8007  tposfun  8297  tpostpos2  8302  fpr3g  8341  wfr3g  8375  tfrlem10  8433  tfrlem12  8435  tfr3  8445  seqomlem1  8498  seqomlem2  8499  seqomlem4  8501  ondif2  8548  oa0  8562  om0  8563  oa1suc  8577  om1  8588  oe1  8590  oe1m  8591  omass  8626  om2  8632  oeoalem  8643  oeoelem  8645  nnmsucr  8672  nnm1  8699  nnm2  8700  naddrid  8731  naddlid  8732  ecelqs  8826  xpider  8847  mapdm0  8900  fvdiagfn  8957  ixpsnf1o  9004  funen1cnv  9094  xp1en  9120  undom  9122  sbthlem7  9150  domunsn  9184  xpmapenlem  9201  infensuc  9212  findcard2d  9220  diffi  9228  cnvfi  9229  enreffi  9236  snnen2o  9274  1sdom2dom  9283  infi  9299  finresfin  9301  unblem1  9322  unblem2  9323  unblem3  9324  unblem4  9325  isfinite2  9328  infn0ALT  9333  unfilem1  9335  unfilem2  9336  unfir  9338  fofinf1o  9359  cnvfiALT  9366  mptfi  9378  finsschain  9386  imafi2  9388  marypha2  9468  inf0  9659  trcl  9766  frr3g  9797  r1rankidb  9849  snwf  9854  unwf  9855  uniwf  9865  rankval3b  9873  rankr1a  9885  rankval4b  9917  rankxplim3  9935  hfuni  9961  scott0b  9974  scott0OLD  9975  djueq1  10023  card1  10086  pm54.43  10121  infxpenc2  10140  dfac8clem  10150  alephsuc2  10198  alephle  10206  cardaleph  10207  dfac12lem2  10262  undjudom  10285  djudom1  10300  pwdju1  10308  nnadju  10315  ackbij1lem18  10353  cflem  10362  cflecard  10369  cfeq0  10373  cfslb  10383  cfsmolem  10387  cfcoflem  10389  cfidm  10392  isfin4p1  10432  fin23lem12  10448  fin23lem16  10452  fin23lem28  10457  fin23lem38  10466  fin23lem41  10469  fin1a2lem7  10523  fin1a2lem12  10528  fin1a2lem13  10529  hsmexlem8  10541  axcc2lem  10553  axcc3  10555  domtriomlem  10559  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  axcclem  10574  ac6num  10596  ttukeylem4  10629  ttukeylem7  10632  ttukey2g  10633  axdclem  10636  brdom3  10646  brdom5  10647  imadomnum  10653  cardeq0  10675  unsnen  10676  konigthlem  10692  pwcfsdom  10707  canthp1lem1  10776  wunex2  10862  wuncval2  10871  eltsk2g  10875  ingru  10939  grutsk  10946  axgroth6  10952  mulidpi  11010  nlt1pi  11030  indpi  11031  pinq  11051  mulidnq  11087  1idpr  11153  prlem934  11157  0idsr  11221  1idsr  11222  00sr  11223  negexsr  11226  recexsrlem  11227  sqgt0sr  11230  ax1rid  11285  axcnre  11288  ne0gt0  11454  peano2cn  11521  peano2re  11522  00id  11524  mul02lem2  11526  mul01  11528  subid  11616  subid1  11617  negid  11644  negeq0  11651  peano2cnm  11663  peano2rem  11664  lt0neg1  11862  le0neg1  11864  relin01  11880  div2neg  12080  recgt0ii  12263  divgt0i2i  12272  ledivp1i  12282  ltdivp1i  12283  inelr  12350  indconst0  12372  indconst1  12373  peano5nni  12378  peano2nn  12387  nnge1  12406  nnne0  12412  times2  12519  addltmul  12622  nn0p1nn  12685  peano2nn0  12686  nn0lele2xi  12702  fcdmnn0supp  12703  fcdmnn0fsupp  12704  fcdmnn0suppg  12705  peano2z  12777  peano2zm  12779  suprzcl  12819  zeo  12825  eluzaddi  13036  uzwo  13078  uzwo2  13079  infssuzle  13098  infssuzcl  13099  zq  13121  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  rphalfcl  13189  zgt1rpn0n1  13203  ltpnf  13289  nltmnf  13298  pnfge  13299  nltpnft  13334  xlemnf  13337  qsqueeze  13371  xlt0neg1  13389  xle0neg1  13391  xaddpnf1  13396  xaddmnf1  13398  xaddrid  13411  xsubge0  13431  xmul01  13437  xmulneg1  13439  xmulpnf1  13444  xmulrid  13449  supxrbnd  13498  supxrgtmnf  13499  supxrre1  13500  supxrre2  13501  elioopnf  13614  elicopnf  13616  iccshftri  13658  iccshftli  13660  iccdili  13662  icccntri  13664  fzprval  13759  fz0add1fz1  13910  fzofzp1  13939  fzostep1  13961  injresinj  13966  flge0nn0  14000  flge1nn  14001  btwnzge0  14008  modfrac  14064  om2uzsuci  14131  axdc4uzlem  14166  ser1const  14241  exp0  14248  exp1  14250  expn1  14254  nn0sqcl  14272  sqval  14297  sqeq0  14303  resqcl  14307  zsqcl  14312  expubnd  14361  binom21  14404  expnbnd  14417  nn0opthlem2  14454  bcnn  14497  bcn2  14504  bcn2p1  14510  bcnm1  14512  hasheq0  14548  hashsng  14554  hashen1  14555  hashunsnggt  14579  hashin  14597  hashdif  14599  hashgt23el  14610  hashxplem  14619  hashf1lem2  14642  hash2pr  14655  hash2prde  14656  pr2pwpr  14665  hash3tr  14677  iswrd  14701  wrdval  14702  hashwrdn  14733  ccatval2  14764  ccatrid  14774  eqs1  14802  s111  14805  ccatws1len  14810  repsw0  14970  repsw1  14976  cshw0  14987  wwlktovf  15152  relexpsucnnl  15226  reim0  15328  imval2  15361  cjne0  15373  abssq  15516  max0add  15520  abs2dif  15543  rddif  15552  absrdbnd  15553  rexuz3  15560  isershft  15875  isercolllem2  15877  isercoll  15879  fsum  15930  fsumadd  15950  fsumsplitsnun  15965  bcxmas  16048  infcvgaux2i  16071  fprod  16152  risefac0  16237  fallfac0  16238  risefac1  16243  fallfac1  16244  bpoly2  16267  bpoly3  16268  bpoly4  16269  fsumcube  16270  efi4p  16349  resin4p  16350  recos4p  16351  sinbnd  16392  cosbnd  16393  rpnnen2lem8  16433  rpnnen2lem12  16437  cnso  16459  dvdsmul2  16492  dvdslelem  16523  odd2np1lem  16554  mod2eq1n2dvds  16561  divalglem0  16607  divalglem1  16608  divalglem4  16610  divalglem5  16611  divalglem8  16614  flodddiv4  16629  bits0  16642  bitsp1o  16647  bitsf1  16660  sadadd2lem2  16664  gcd1  16745  lcm0val  16813  dvdslcm  16817  lcmeq0  16819  lcmgcd  16826  lcm1  16829  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  prm2orodd  16910  phiprm  16998  pc0  17076  pcdvdstr  17098  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  hashbc0  17227  setsval  17389  fsets  17391  setsres  17400  ressinbas  17467  ressress  17469  elrestr  17649  pwssnf1o  17720  xpsfrnel  17784  xpscf  17787  ismred2  17823  submre  17825  mreacs  17882  oppchomfval  17938  brssc  18039  isssc  18045  yonedalem4c  18501  oduleval  18513  isprs  18520  oduclatb  18731  chninf  18859  gsumval2a  18924  smndex1n0mnd  19161  mulg1  19341  mulgnegnn  19344  qusxpid  19445  ghmghmrn  19499  cntrnsg  19609  oppgplusfval  19613  pgrpsubgsymg  19674  psgneldm2i  19770  efgrelexlemb  20015  frgp0  20025  frgpmhm  20030  vrgpf  20033  cntrcmnd  20107  cntrabl  20108  cygctb  20157  dprd0  20298  dprd2da  20309  mgpplusg  20415  opprmulfval  20620  subrngint  20863  subrgint  20898  lsp0  21335  rlmval2  21518  cncrng  21751  cnfld1  21755  zringcyg  21830  mulgrhm2  21839  zlmsca  21881  fermltlchr  21890  chrnzr  21891  zrhpsgnelbas  21955  ocvz  22039  cssincl  22049  css0  22050  css1  22051  frlmip  22139  fczpsrbag  22284  evls1rhmlem  22694  evl1fval1lem  22703  marrepeval  22933  matunitlindflem2  23050  decpmatid  23143  0opn  23277  topopn  23279  basdif0  23326  tgval  23328  isopn2  23405  0cld  23411  ntropn  23422  ntrval2  23424  ntrdif  23425  clsdif  23426  cmclsopn  23435  ntrtop  23443  ntr0  23454  mretopd  23465  neips  23486  neiptopnei  23505  maxlp  23520  isperf2  23525  rest0  23542  iocpnfordt  23588  icomnfordt  23589  mnfnei  23594  refref  23887  unisngl  23901  1stckgen  23928  ptbasfi  23955  pthaus  24012  fbssfi  24211  isfil2  24230  ssfg  24246  filconn  24257  fbasrn  24258  filufint  24294  imaelfm  24325  fmfnfmlem4  24331  fclsfnflim  24401  alexsubALTlem3  24423  alexsubALTlem4  24424  ustfilxp  24587  ustuqtop2  24616  ustuqtop4  24618  utopsnneiplem  24621  utopsnnei  24623  utop2nei  24624  cfiluweak  24668  neipcfilu  24669  xmetres  24738  metres  24739  mopnex  24893  prdsms  24905  metucn  24945  tngds  25022  tngngp3  25030  nmoge0  25095  cnfldnm  25152  tgioo  25170  xrtgioo  25181  xrsmopn  25187  negcncf  25298  phtpy01  25361  pco0  25390  tcphtopn  25602  tchnmfval  25604  caussi  25673  rrxip  25766  minveclem3b  25804  ovolfioo  25843  ovolficc  25844  ovolfsf  25847  ovolctb  25866  ovolctb2  25868  ovolfiniun  25877  ovoliun2  25882  ovolshftlem1  25885  ovolscalem1  25889  ovolicopnf  25900  iunmbl2  25933  uniioombllem2  25959  opnmblALT  25979  ismbf  26004  mbfinf  26041  0plef  26048  itg1climres  26090  itg2cnlem1  26137  iblitg  26144  ibl0  26162  itgcn  26220  cnlimc  26263  dvfre  26326  dvnfre  26327  dveflem  26354  dvef  26355  dvlipcn  26369  lhop2  26390  itgsubstlem  26423  deg1val  26469  ply1rem  26539  coefv0  26622  plyrecj  26653  rnplynfin  26685  vieta1lem2  26689  aannenlem1  26712  aaliou2b  26725  ulmval  26764  ulmpm  26767  ulmdvlem1  26784  mtest  26788  efcn  26827  sin2pim  26871  cos2pim  26872  sinmpi  26873  cosmpi  26874  sinppi  26875  cosppi  26876  efimpi  26877  sincosq1lem  26883  sincosq2sgn  26885  sincosq3sgn  26886  sincosq4sgn  26887  sinq12gt0  26893  sinq34lt0t  26895  sincosq1eq  26898  abssinper  26906  efif1o  26931  loglt1b  27019  relogcn  27023  ellogdm  27024  efopn  27043  cxp0  27055  cxp1  27056  cxpsqrt  27088  logsqrt  27089  logb1  27154  atandm3  27263  atanbnd  27311  atancn  27321  leibpi  27327  efrlim  27354  logdifbnd  27378  vmaprm  27501  ppip1le  27545  ppieq0  27560  prmorcht  27562  ppiublem1  27586  ppiub  27588  chpeq0  27592  chtub  27596  fsumvma  27597  pclogsum  27599  chpval2  27602  dchrresb  27643  dchrptlem1  27648  lgs0  27694  lgs2  27698  lgsdir2lem2  27710  lgsdir2lem4  27712  lgsdchrval  27738  lgsdchr  27739  lgseisenlem2  27760  2lgslem1c  27777  2lgsoddprmlem2  27793  addsq2nreurex  27828  dirith2  27912  selberg2lem  27934  qabvle  28009  qabvexp  28010  ostth  28023  noextendseq  28081  noetasuplem4  28150  noetainflem4  28154  cutsun12  28233  madebdayim  28331  bdayiun  28358  addsrid  28407  addsfo  28426  peano2no  28427  negscl  28479  subsfo  28508  subsid1  28511  muls01  28555  mulsrid  28556  divs1  28647  recsex  28662  abssnid  28686  peano2ons  28723  noseqp1  28734  noseqind  28735  peano2nns  28793  n0fincut  28798  n0lts1e0  28811  dfnns2  28815  oldfib  28820  elzs2  28842  elnnzs  28844  elznns  28845  zsoring  28852  n0seo  28864  exps0  28870  exps1  28871  bdaypw2n0bndlem  28906  bdayfin  28930  istrkg2ld  28979  istrkg3ld  28980  ttgval  29509  brbtwn  29534  colinearalglem4  29544  upgr0eop  29749  uspgrushgr  29815  usgruspgr  29818  usgr0eop  29884  0grsubgr  29916  uspgrloopvtx  30153  umgr2v2evtx  30159  usgr0edg0rusgr  30213  rgrusgrprc  30227  wlkvtxiedg  30262  pthdivtx  30369  usgr2pthlem  30406  wlkswwlksf1o  30525  wwlksext2clwwlk  30705  loop1cycl  30801  konigsbergssiedgw  30908  frgrncvvdeqlem7  30963  2clwwlk2  31006  ex-po  31093  pliguhgr  31145  nvnd  31347  ipval2lem3  31364  ipval2  31366  ipidsq  31369  dipcj  31373  dip0r  31376  nmlnogt0  31456  blocni  31464  ipasslem2  31491  ipasslem8  31496  ipasslem9  31497  ajval  31520  ubthlem1  31529  hvaddlid  31682  hvsub0  31735  hi02  31756  hlimi  31847  isch2  31882  chlimi  31893  chsupunss  32003  shsupunss  32005  chlejb1i  32135  h1dei  32209  h1de2ci  32215  spanunsni  32238  pjoml2i  32244  pjorthi  32328  mayete3i  32387  hosubid1  32457  nmopge0  32570  nmfnge0  32586  adj1  32592  adjeq  32594  lnop0  32625  lnopmi  32659  nmophmi  32690  cnlnadjlem5  32730  cnlnadjeui  32736  unierri  32763  leoprf2  32786  leopnmid  32797  nmopleid  32798  hstles  32890  hst0  32892  strlem3a  32911  dmdbr2  32962  mdsl1i  32980  mdsl2i  32981  mdsl2bi  32982  cvmdi  32983  mdslmd1lem1  32984  mdslmd1lem2  32985  mdslmd1i  32988  mdslmd2i  32989  csmdsymi  32993  mdexchi  32994  superpos  33013  atomli  33041  atordi  33043  chirredlem1  33049  chirredlem2  33050  atcvat4i  33056  atabsi  33060  mdsymlem1  33062  mdsymlem5  33066  mdsymlem6  33067  sumdmdii  33074  dmdbr5ati  33081  dmdbr6ati  33082  mddmdin0i  33090  cdj3lem2  33094  unidifsnel  33229  unidifsnne  33230  xppreima  33337  abfmpunirn  33344  abfmpel  33347  aciunf1lem  33354  fgreu  33363  padct  33407  fpwrelmapffslem  33420  fpwrelmap  33421  xrge0infss  33448  xrdifh  33468  pfx1s2  33602  clatp0cl  33633  clatp1cl  33634  cntrcrng  33741  cycpmco2lem4  33789  rmfsupp2  33897  1fldgenq  33988  resvval  33994  rearchi  34011  opprabs  34110  zringfrac  34189  psrbasfsupp  34254  0mplrim  34257  rlmdim  34353  constrfiss  34494  2sqr3minply  34523  locfinreflem  34583  locfinref  34584  ordtconnlem1  34667  rge0scvg  34692  lmxrge0  34695  qqh0  34727  qqh1  34728  rrh0  34758  zrhre  34762  esumcst  34806  esumfzf  34812  esumfsupre  34814  hasheuni  34828  sgon  34867  dmvlsiga  34872  sigainb  34880  measval  34942  ismeas  34943  sxbrsigalem0  35014  omssubadd  35043  carsggect  35061  eulerpartlemmf  35118  eulerpartlemgs2  35123  eulerpartlemn  35124  rrvsum  35197  ballotlem2  35232  ballotlemfcc  35237  ballotlem4  35242  signsplypnf  35290  signsply0  35291  signsw0glem  35293  signswrid  35298  signlem0  35327  signshf  35328  bnj535  35631  bnj580  35654  bnj907  35708  bnj1253  35758  trscott  35883  rncardr1prc  35891  fineqvnttrclse  35933  noinfepfnregs  35941  j0le  36060  k3n0j0lt  36061  jltalephlem  36066  jltaleph  36067  onvf1odlem1  36072  onvf1od  36076  ptpconn  36206  cvmsss2  36247  cvmlift2lem12  36287  cvmlift2lem13  36288  cvmliftphtlem  36290  cvmliftpht  36291  fmlafvel  36358  mppsthm  36552  elpssmo  36673  bcneg1  36716  fv1stcnv  36756  fv2ndcnv  36757  wlimeq1  36797  imagesset  36932  altopeq1  36943  brcolinear2  37038  nmulr0  37159  nmull0  37160  nmulrid  37161  cldbnd  37329  ivthALT  37338  refssfne  37361  ontgval  37434  onint1  37452  ttcid  37495  ttcss  37501  ttcss2  37502  ttcsnexg  37523  ttcwf  37527  dfttc4lem2  37532  ttc0el  37538  axc11n11r  37800  bj-pm11.53a  37887  bj-bm1.3ii  38249  bj-restsn0  38276  bj-restsn10  38277  bj-restsnid  38278  bj-rest10  38279  bj-rest0  38284  bj-inftyexpiinv  38397  bj-inftyexpidisj  38399  taupilem1  38510  irrdiff  38515  qdiff  38516  f1omptsnlem  38527  mptsnunlem  38529  topdifinffinlem  38538  inunissunidif  38566  rdgssun  38569  exrecfnlem  38570  exrecfnpw  38572  finixpnum  38796  tan2h  38803  ptrest  38805  poimirlem22  38828  poimirlem25  38831  mblfinlem1  38843  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  ftc1anclem5  38883  ftc1anclem8  38886  dvasin  38890  dvacos  38891  sdclem2  38942  totbndbnd  38989  heibor1lem  39009  heiborlem7  39017  bfplem1  39022  prnc  39267  brxrn  39581  ecxrn2  39606  dfpeters2  40172  riotasv  40282  glbconN  40700  atpointN  41066  polsubN  41230  pol0N  41232  pol1N  41233  2polvalN  41237  2polssN  41238  3polN  41239  pcl0N  41245  2pmaplubN  41249  pnonsingN  41256  polsubclN  41275  cdlemefs32sn1aw  41737  cdleme43fsv1snlem  41743  cdleme41sn3a  41756  cdleme32a  41764  cdleme40m  41790  cdleme40n  41791  cdleme42b  41801  istendo  42083  cdlemk40  42240  cdlemkid  42259  dihvalcqpre  42558  facp2  43459  relt0neg1  43786  sn-nnne0  43790  frlmsnic  43870  prjspnerlem  43911  prjspnval2  43912  0prjspn  43930  3cubes  43966  mapfzcons1cl  43995  eldioph3b  44042  eldiophss  44051  0dioph  44055  vdioph  44056  eldioph4b  44084  eldioph4i  44085  rencldnfilem  44093  rmxy1  44195  rmxy0  44196  rmxm1  44207  rmym1  44208  monotoddzzfi  44215  wepwso  44316  aomclem6  44327  pwslnmlem0  44359  isnumbasabl  44373  areaquad  44479  onexlimgt  44506  oaabsb  44557  nadd1suc  44655  oe2  44668  safesnsupfidom1o  44679  onnoxp  44695  oa1cl  44709  finona1cl  44715  reabsifneg  44893  reabsifnneg  44896  relexp2  44938  eltrclrec  44941  elrtrclrec  44942  brtrclrec  44957  brrtrclrec  44958  relexpxpmin  44978  dftrcl3  44981  dfrtrcl3  44994  heeq1  45038  seff  45554  lhe4.4ex1a  45574  eelT0  46017  snssl  46072  sineq0ALT  46179  trfr  46216  xpwf  46218  dmwf  46219  rnwf  46220  modelaxreplem1  46232  modelaxreplem3  46234  0elaxnul  46237  prclaxpr  46239  uniclaxun  46240  wfac8prim  46256  permaxinf2lem  46266  hashnnsuc  46274  elrnmpt1sf  46477  founiiun0  46478  supxrgere  46618  supxrgelem  46622  fmuldfeqlem1  46867  fmuldfeq  46868  climneg  46895  sumnnodd  46915  liminfltlem  47087  xlimpnfxnegmnf2  47141  addccncf2  47159  dvsinax  47196  stoweidlem18  47301  stoweidlem19  47302  stoweidlem22  47305  stoweidlem34  47317  stoweidlem40  47323  stoweidlem41  47324  stoweidlem55  47338  stoweidlem59  47342  dirker2re  47375  dirkerdenne0  47376  fourierdlem48  47437  fourierdlem49  47438  fourierdlem70  47459  fourierdlem71  47460  fourierdlem104  47493  fourierdlem112  47501  fouriersw  47514  etransclem46  47563  etransclem48  47565  nnfoctbdjlem  47738  ormklocald  48159  cjnpoly  48212  sinnpoly  48214  sqrtrrnpoly  48215  sqrtnegnre  48650  fsummmodsnunz  48726  flsqrt5  48952  bits0ALTV  49050  mogoldbblem  49091  sgoldbeven3prm  49154  nnsum3primes4  49159  isubgr0uhgr  49244  ushggricedg  49298  2zrngnmlid  49625  2zrngnmrid  49626  adcnellaz  49732  mpoexxg2  49781  lco0  49870  zlmodzxzldeplem3  49945  0dig1  50052  naryfvalel  50073  ackvalsuc0val  50130  iinxp  50273  0funclem  50532  parswapprop  51108  aacllem  51367