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  1482  elvd  3456  elabg  3629  eueq2  3667  sbcgf  3808  sbcralg  3820  csbconstgf  3864  sbcnestgw  4380  csbnestgw  4381  sbcnestg  4385  csbnestg  4386  csbnest1g  4389  ssex  5281  iinexg  5308  eusv2nf  5356  reusv2lem5  5363  nnullss  5429  xpss1  5669  xpiindi  5811  reldm0  5909  elrnmpt1s  5940  resdm  6014  eliniseg  6091  trinxp  6118  ssrnres  6169  cnveq0  6190  coi2  6265  relrelss  6275  relresfld  6278  cnviin  6289  elpred  6321  onelssex  6412  ord0eln0  6419  funcnvres  6618  funimaex  6627  fnresin1  6664  fnresin2  6665  fresin  6751  ssimaex  6970  fvmpt  6993  fvmptnf  7016  fvimacnvALT  7056  dff3  7100  fsn  7136  fsn2  7137  funop  7153  fvrnressn  7165  fnsnbg  7169  fninfp  7179  fndifnfp  7181  fnnfpeq0  7183  fprb  7199  elabrex  7246  elabrexg  7247  f1elima  7267  f1ofvswap  7314  fliftel1  7318  f1owe  7361  f1oweOLD  7362  sorpssuni  7748  sorpssint  7749  eldifpw  7782  ordeleqon  7796  ordsson  7797  ssnlim  7897  abrexexg  7973  tposfun  8259  tpostpos2  8264  fpr3g  8303  wfr3g  8337  tfrlem10  8395  tfrlem12  8397  tfr3  8407  seqomlem1  8460  seqomlem2  8461  seqomlem4  8463  ondif2  8510  oa0  8524  om0  8525  oa1suc  8539  om1  8550  oe1  8552  oe1m  8553  omass  8588  om2  8594  oeoalem  8605  oeoelem  8607  nnmsucr  8634  nnm1  8661  nnm2  8662  naddrid  8693  naddlid  8694  ecelqs  8788  xpider  8809  mapdm0  8862  fvdiagfn  8919  ixpsnf1o  8966  funen1cnv  9056  xp1en  9082  undom  9084  sbthlem7  9112  domunsn  9146  xpmapenlem  9163  infensuc  9174  findcard2d  9182  diffi  9190  cnvfi  9191  enreffi  9198  snnen2o  9236  1sdom2dom  9245  infi  9261  finresfin  9263  unblem1  9284  unblem2  9285  unblem3  9286  unblem4  9287  isfinite2  9290  infn0ALT  9295  unfilem1  9297  unfilem2  9298  unfir  9300  fofinf1o  9321  cnvfiALT  9328  mptfi  9340  finsschain  9348  imafi2  9350  marypha2  9431  inf0  9622  trcl  9729  frr3g  9760  r1rankidb  9812  snwf  9817  unwf  9818  uniwf  9828  rankval3b  9836  rankr1a  9848  rankval4b  9880  rankxplim3  9898  hfuni  9924  scott0b  9937  scott0OLD  9938  djueq1  9986  card1  10049  pm54.43  10082  infxpenc2  10101  dfac8clem  10111  alephsuc2  10159  alephle  10167  cardaleph  10168  dfac12lem2  10223  undjudom  10246  djudom1  10261  pwdju1  10269  nnadju  10276  ackbij1lem18  10314  cflem  10323  cflecard  10330  cfeq0  10334  cfslb  10344  cfsmolem  10348  cfcoflem  10350  cfidm  10353  isfin4p1  10393  fin23lem12  10409  fin23lem16  10413  fin23lem28  10418  fin23lem38  10427  fin23lem41  10430  fin1a2lem7  10484  fin1a2lem12  10489  fin1a2lem13  10490  hsmexlem8  10502  axcc2lem  10514  axcc3  10516  domtriomlem  10520  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  axcclem  10535  ac6num  10557  ttukeylem4  10590  ttukeylem7  10593  ttukey2g  10594  axdclem  10597  brdom3  10607  brdom5  10608  imadomnum  10614  cardeq0  10636  unsnen  10637  konigthlem  10653  pwcfsdom  10668  canthp1lem1  10737  wunex2  10823  wuncval2  10832  eltsk2g  10836  ingru  10900  grutsk  10907  axgroth6  10913  mulidpi  10971  nlt1pi  10991  indpi  10992  pinq  11012  mulidnq  11048  1idpr  11114  prlem934  11118  0idsr  11182  1idsr  11183  00sr  11184  negexsr  11187  recexsrlem  11188  sqgt0sr  11191  ax1rid  11246  axcnre  11249  ne0gt0  11415  peano2cn  11482  peano2re  11483  00id  11485  mul02lem2  11487  mul01  11489  subid  11577  subid1  11578  negid  11605  negeq0  11612  peano2cnm  11624  peano2rem  11625  lt0neg1  11822  le0neg1  11824  relin01  11840  div2neg  12040  recgt0ii  12223  divgt0i2i  12232  ledivp1i  12242  ltdivp1i  12243  inelr  12310  indconst0  12332  indconst1  12333  peano5nni  12338  peano2nn  12347  nnge1  12366  nnne0  12372  times2  12479  addltmul  12582  nn0p1nn  12645  peano2nn0  12646  nn0lele2xi  12662  fcdmnn0supp  12663  fcdmnn0fsupp  12664  fcdmnn0suppg  12665  peano2z  12737  peano2zm  12739  suprzcl  12779  zeo  12785  eluzaddi  12996  uzwo  13038  uzwo2  13039  infssuzle  13058  infssuzcl  13059  zq  13081  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  rphalfcl  13149  zgt1rpn0n1  13163  ltpnf  13249  nltmnf  13258  pnfge  13259  nltpnft  13294  xlemnf  13297  qsqueeze  13331  xlt0neg1  13349  xle0neg1  13351  xaddpnf1  13356  xaddmnf1  13358  xaddrid  13371  xsubge0  13391  xmul01  13397  xmulneg1  13399  xmulpnf1  13404  xmulrid  13409  supxrbnd  13458  supxrgtmnf  13459  supxrre1  13460  supxrre2  13461  elioopnf  13574  elicopnf  13576  iccshftri  13618  iccshftli  13620  iccdili  13622  icccntri  13624  fzprval  13719  fz0add1fz1  13870  fzofzp1  13899  fzostep1  13921  injresinj  13926  flge0nn0  13960  flge1nn  13961  btwnzge0  13968  modfrac  14024  om2uzsuci  14091  axdc4uzlem  14126  ser1const  14201  exp0  14208  exp1  14210  expn1  14214  nn0sqcl  14232  sqval  14257  sqeq0  14263  resqcl  14267  zsqcl  14272  expubnd  14321  binom21  14363  expnbnd  14376  nn0opthlem2  14413  bcnn  14456  bcn2  14463  bcn2p1  14469  bcnm1  14471  hasheq0  14507  hashsng  14513  hashen1  14514  hashunsnggt  14538  hashin  14556  hashdif  14558  hashgt23el  14569  hashxplem  14578  hashf1lem2  14601  hash2pr  14614  hash2prde  14615  pr2pwpr  14624  hash3tr  14636  iswrd  14660  wrdval  14661  hashwrdn  14692  ccatval2  14723  ccatrid  14733  eqs1  14760  s111  14763  ccatws1len  14768  repsw0  14928  repsw1  14934  cshw0  14945  wwlktovf  15109  relexpsucnnl  15183  reim0  15285  imval2  15318  cjne0  15330  abssq  15473  max0add  15477  abs2dif  15500  rddif  15508  absrdbnd  15509  rexuz3  15516  isershft  15831  isercolllem2  15833  isercoll  15835  fsum  15886  fsumadd  15906  fsumsplitsnun  15921  bcxmas  16004  infcvgaux2i  16027  fprod  16108  risefac0  16193  fallfac0  16194  risefac1  16199  fallfac1  16200  bpoly2  16223  bpoly3  16224  bpoly4  16225  fsumcube  16226  efi4p  16305  resin4p  16306  recos4p  16307  sinbnd  16348  cosbnd  16349  rpnnen2lem8  16389  rpnnen2lem12  16393  cnso  16415  dvdsmul2  16448  dvdslelem  16479  odd2np1lem  16510  mod2eq1n2dvds  16517  divalglem0  16563  divalglem1  16564  divalglem4  16566  divalglem5  16567  divalglem8  16570  flodddiv4  16585  bits0  16598  bitsp1o  16603  bitsf1  16616  sadadd2lem2  16620  gcd1  16701  lcm0val  16769  dvdslcm  16773  lcmeq0  16775  lcmgcd  16782  lcm1  16785  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  prm2orodd  16866  phiprm  16954  pc0  17032  pcdvdstr  17054  vdwlem2  17160  vdwlem6  17164  vdwlem8  17166  hashbc0  17183  setsval  17345  fsets  17347  setsres  17356  ressinbas  17423  ressress  17425  elrestr  17599  pwssnf1o  17670  xpsfrnel  17734  xpscf  17737  ismred2  17773  submre  17775  mreacs  17832  oppchomfval  17888  brssc  17989  isssc  17995  yonedalem4c  18451  oduleval  18463  isprs  18470  oduclatb  18681  chninf  18809  gsumval2a  18874  smndex1n0mnd  19111  mulg1  19291  mulgnegnn  19294  qusxpid  19395  ghmghmrn  19449  cntrnsg  19558  oppgplusfval  19562  pgrpsubgsymg  19623  psgneldm2i  19719  efgrelexlemb  19964  frgp0  19974  frgpmhm  19979  vrgpf  19982  cntrcmnd  20056  cntrabl  20057  cygctb  20106  dprd0  20247  dprd2da  20258  mgpplusg  20364  opprmulfval  20569  subrngint  20812  subrgint  20847  lsp0  21284  rlmval2  21467  cncrng  21699  cnfld1  21703  zringcyg  21775  mulgrhm2  21784  zlmsca  21826  fermltlchr  21835  chrnzr  21836  zrhpsgnelbas  21900  ocvz  21984  cssincl  21994  css0  21995  css1  21996  frlmip  22084  fczpsrbag  22229  evls1rhmlem  22639  evl1fval1lem  22648  marrepeval  22878  matunitlindflem2  22995  decpmatid  23088  0opn  23222  topopn  23224  basdif0  23271  tgval  23273  isopn2  23350  0cld  23356  ntropn  23367  ntrval2  23369  ntrdif  23370  clsdif  23371  cmclsopn  23380  ntrtop  23388  ntr0  23399  mretopd  23410  neips  23431  neiptopnei  23450  maxlp  23465  isperf2  23470  rest0  23487  iocpnfordt  23533  icomnfordt  23534  mnfnei  23539  refref  23832  unisngl  23846  1stckgen  23873  ptbasfi  23900  pthaus  23957  fbssfi  24156  isfil2  24175  ssfg  24191  filconn  24202  fbasrn  24203  filufint  24239  imaelfm  24270  fmfnfmlem4  24276  fclsfnflim  24346  alexsubALTlem3  24368  alexsubALTlem4  24369  ustfilxp  24532  ustuqtop2  24561  ustuqtop4  24563  utopsnneiplem  24566  utopsnnei  24568  utop2nei  24569  cfiluweak  24613  neipcfilu  24614  xmetres  24683  metres  24684  mopnex  24838  prdsms  24850  metucn  24890  tngds  24967  tngngp3  24975  nmoge0  25040  cnfldnm  25097  tgioo  25115  xrtgioo  25126  xrsmopn  25132  negcncf  25243  phtpy01  25306  pco0  25335  tcphtopn  25547  tchnmfval  25549  caussi  25618  rrxip  25711  minveclem3b  25749  ovolfioo  25788  ovolficc  25789  ovolfsf  25792  ovolctb  25811  ovolctb2  25813  ovolfiniun  25822  ovoliun2  25827  ovolshftlem1  25830  ovolscalem1  25834  ovolicopnf  25845  iunmbl2  25878  uniioombllem2  25904  opnmblALT  25924  ismbf  25949  mbfinf  25986  0plef  25993  itg1climres  26035  itg2cnlem1  26082  iblitg  26089  ibl0  26107  itgcn  26165  cnlimc  26208  dvfre  26271  dvnfre  26272  dveflem  26299  dvef  26300  dvlipcn  26314  lhop2  26335  itgsubstlem  26368  deg1val  26414  ply1rem  26484  coefv0  26567  plyrecj  26598  rnplynfin  26630  vieta1lem2  26634  aannenlem1  26655  aaliou2b  26668  ulmval  26707  ulmpm  26710  ulmdvlem1  26727  mtest  26731  efcn  26770  sin2pim  26814  cos2pim  26815  sinmpi  26816  cosmpi  26817  sinppi  26818  cosppi  26819  efimpi  26820  sincosq1lem  26826  sincosq2sgn  26828  sincosq3sgn  26829  sincosq4sgn  26830  sinq12gt0  26836  sinq34lt0t  26838  sincosq1eq  26841  abssinper  26849  efif1o  26874  loglt1b  26962  relogcn  26966  ellogdm  26967  efopn  26986  cxp0  26998  cxp1  26999  cxpsqrt  27031  logsqrt  27032  logb1  27097  atandm3  27206  atanbnd  27254  atancn  27264  leibpi  27270  efrlim  27297  logdifbnd  27321  vmaprm  27444  ppip1le  27488  ppieq0  27503  prmorcht  27505  ppiublem1  27529  ppiub  27531  chpeq0  27535  chtub  27539  fsumvma  27540  pclogsum  27542  chpval2  27545  dchrresb  27586  dchrptlem1  27591  lgs0  27637  lgs2  27641  lgsdir2lem2  27653  lgsdir2lem4  27655  lgsdchrval  27681  lgsdchr  27682  lgseisenlem2  27703  2lgslem1c  27720  2lgsoddprmlem2  27736  addsq2nreurex  27771  dirith2  27855  selberg2lem  27877  qabvle  27952  qabvexp  27953  ostth  27966  noextendseq  28024  noetasuplem4  28093  noetainflem4  28097  cutsun12  28176  madebdayim  28274  bdayiun  28301  addsrid  28350  addsfo  28369  peano2no  28370  negscl  28422  subsfo  28451  subsid1  28454  muls01  28498  mulsrid  28499  divs1  28590  recsex  28605  abssnid  28629  peano2ons  28666  noseqp1  28677  noseqind  28678  peano2nns  28736  n0fincut  28741  n0lts1e0  28754  dfnns2  28758  oldfib  28763  elzs2  28785  elnnzs  28787  elznns  28788  zsoring  28795  n0seo  28807  exps0  28813  exps1  28814  bdaypw2n0bndlem  28849  bdayfin  28873  istrkg2ld  28922  istrkg3ld  28923  ttgval  29452  brbtwn  29477  colinearalglem4  29487  upgr0eop  29692  uspgrushgr  29758  usgruspgr  29761  usgr0eop  29827  0grsubgr  29859  uspgrloopvtx  30096  umgr2v2evtx  30102  usgr0edg0rusgr  30156  rgrusgrprc  30170  wlkvtxiedg  30205  pthdivtx  30312  usgr2pthlem  30349  wlkswwlksf1o  30468  wwlksext2clwwlk  30648  loop1cycl  30744  konigsbergssiedgw  30851  frgrncvvdeqlem7  30906  2clwwlk2  30949  ex-po  31036  pliguhgr  31088  nvnd  31290  ipval2lem3  31307  ipval2  31309  ipidsq  31312  dipcj  31316  dip0r  31319  nmlnogt0  31399  blocni  31407  ipasslem2  31434  ipasslem8  31439  ipasslem9  31440  ajval  31463  ubthlem1  31472  hvaddlid  31625  hvsub0  31678  hi02  31699  hlimi  31790  isch2  31825  chlimi  31836  chsupunss  31946  shsupunss  31948  chlejb1i  32078  h1dei  32152  h1de2ci  32158  spanunsni  32181  pjoml2i  32187  pjorthi  32271  mayete3i  32330  hosubid1  32400  nmopge0  32513  nmfnge0  32529  adj1  32535  adjeq  32537  lnop0  32568  lnopmi  32602  nmophmi  32633  cnlnadjlem5  32673  cnlnadjeui  32679  unierri  32706  leoprf2  32729  leopnmid  32740  nmopleid  32741  hstles  32833  hst0  32835  strlem3a  32854  dmdbr2  32905  mdsl1i  32923  mdsl2i  32924  mdsl2bi  32925  cvmdi  32926  mdslmd1lem1  32927  mdslmd1lem2  32928  mdslmd1i  32931  mdslmd2i  32932  csmdsymi  32936  mdexchi  32937  superpos  32956  atomli  32984  atordi  32986  chirredlem1  32992  chirredlem2  32993  atcvat4i  32999  atabsi  33003  mdsymlem1  33005  mdsymlem5  33009  mdsymlem6  33010  sumdmdii  33017  dmdbr5ati  33024  dmdbr6ati  33025  mddmdin0i  33033  cdj3lem2  33037  unidifsnel  33131  unidifsnne  33132  xppreima  33239  abfmpunirn  33246  abfmpel  33249  aciunf1lem  33256  fgreu  33265  padct  33310  fpwrelmapffslem  33324  fpwrelmap  33325  xrge0infss  33352  xrdifh  33372  pfx1s2  33506  clatp0cl  33537  clatp1cl  33538  cntrcrng  33642  cycpmco2lem4  33690  rmfsupp2  33798  1fldgenq  33884  resvval  33890  rearchi  33907  opprabs  34006  zringfrac  34086  psrbasfsupp  34143  0mplrim  34146  rlmdim  34242  constrfiss  34383  2sqr3minply  34412  locfinreflem  34472  locfinref  34473  ordtconnlem1  34556  rge0scvg  34581  lmxrge0  34584  qqh0  34616  qqh1  34617  rrh0  34647  zrhre  34651  esumcst  34695  esumfzf  34701  esumfsupre  34703  hasheuni  34717  sgon  34756  dmvlsiga  34761  sigainb  34769  measval  34831  ismeas  34832  sxbrsigalem0  34903  omssubadd  34932  carsggect  34950  eulerpartlemmf  35007  eulerpartlemgs2  35012  eulerpartlemn  35013  rrvsum  35086  ballotlem2  35121  ballotlemfcc  35126  ballotlem4  35131  signsplypnf  35179  signsply0  35180  signsw0glem  35182  signswrid  35187  signlem0  35216  signshf  35217  bnj535  35520  bnj580  35543  bnj907  35597  bnj1253  35647  rncardr1prc  35758  fineqvnttrclse  35792  noinfepfnregs  35800  onvf1odlem1  35882  onvf1od  35886  ptpconn  35998  cvmsss2  36039  cvmlift2lem12  36079  cvmlift2lem13  36080  cvmliftphtlem  36082  cvmliftpht  36083  fmlafvel  36150  mppsthm  36344  bcneg1  36501  fv1stcnv  36541  fv2ndcnv  36542  wlimeq1  36582  imagesset  36717  altopeq1  36728  brcolinear2  36823  nmulr0  36944  nmull0  36945  nmulrid  36946  cldbnd  37114  ivthALT  37123  refssfne  37146  ontgval  37219  onint1  37237  ttcid  37280  ttcss  37286  ttcss2  37287  ttcsnexg  37308  ttcwf  37312  dfttc4lem2  37317  ttc0el  37323  axc11n11r  37585  bj-pm11.53a  37672  bj-bm1.3ii  37979  bj-restsn0  38006  bj-restsn10  38007  bj-restsnid  38008  bj-rest10  38009  bj-rest0  38014  bj-inftyexpiinv  38130  bj-inftyexpidisj  38132  taupilem1  38243  irrdiff  38248  qdiff  38249  f1omptsnlem  38260  mptsnunlem  38262  topdifinffinlem  38271  inunissunidif  38299  rdgssun  38302  exrecfnlem  38303  exrecfnpw  38305  finixpnum  38529  tan2h  38536  ptrest  38538  poimirlem22  38561  poimirlem25  38564  mblfinlem1  38576  mblfinlem2  38577  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  itg2addnclem  38590  itg2addnclem2  38591  itg2addnclem3  38592  itg2addnc  38593  itg2gt0cn  38594  ftc1anclem5  38616  ftc1anclem8  38619  dvasin  38623  dvacos  38624  sdclem2  38677  totbndbnd  38724  heibor1lem  38744  heiborlem7  38752  bfplem1  38757  prnc  39002  brxrn  39316  ecxrn2  39341  dfpeters2  39907  riotasv  40017  glbconN  40435  atpointN  40801  polsubN  40965  pol0N  40967  pol1N  40968  2polvalN  40972  2polssN  40973  3polN  40974  pcl0N  40980  2pmaplubN  40984  pnonsingN  40991  polsubclN  41010  cdlemefs32sn1aw  41472  cdleme43fsv1snlem  41478  cdleme41sn3a  41491  cdleme32a  41499  cdleme40m  41525  cdleme40n  41526  cdleme42b  41536  istendo  41818  cdlemk40  41975  cdlemkid  41994  dihvalcqpre  42293  facp2  43194  relt0neg1  43521  sn-nnne0  43525  frlmsnic  43605  prjspnerlem  43646  prjspnval2  43647  0prjspn  43665  3cubes  43701  mapfzcons1cl  43729  eldioph3b  43776  eldiophss  43785  0dioph  43789  vdioph  43790  eldioph4b  43818  eldioph4i  43819  rencldnfilem  43827  rmxy1  43929  rmxy0  43930  rmxm1  43941  rmym1  43942  monotoddzzfi  43949  wepwso  44050  aomclem6  44061  pwslnmlem0  44093  isnumbasabl  44108  areaquad  44218  onexlimgt  44245  oaabsb  44296  nadd1suc  44394  oe2  44407  safesnsupfidom1o  44418  onnoxp  44434  oa1cl  44448  finona1cl  44454  reabsifneg  44632  reabsifnneg  44635  relexp2  44677  eltrclrec  44680  elrtrclrec  44681  brtrclrec  44696  brrtrclrec  44697  relexpxpmin  44717  dftrcl3  44720  dfrtrcl3  44733  heeq1  44777  seff  45293  lhe4.4ex1a  45313  eelT0  45757  snssl  45812  sineq0ALT  45919  trfr  45952  xpwf  45954  dmwf  45955  rnwf  45956  modelaxreplem1  45968  modelaxreplem3  45970  0elaxnul  45973  prclaxpr  45975  uniclaxun  45976  wfac8prim  45992  permaxinf2lem  46002  hashnnsuc  46010  elrnmpt1sf  46204  founiiun0  46205  supxrgere  46345  supxrgelem  46349  fmuldfeqlem1  46594  fmuldfeq  46595  climneg  46622  sumnnodd  46642  liminfltlem  46814  xlimpnfxnegmnf2  46868  addccncf2  46886  dvsinax  46923  stoweidlem18  47028  stoweidlem19  47029  stoweidlem22  47032  stoweidlem34  47044  stoweidlem40  47050  stoweidlem41  47051  stoweidlem55  47065  stoweidlem59  47069  dirker2re  47102  dirkerdenne0  47103  fourierdlem48  47164  fourierdlem49  47165  fourierdlem70  47186  fourierdlem71  47187  fourierdlem104  47220  fourierdlem112  47228  fouriersw  47241  etransclem46  47290  etransclem48  47292  nnfoctbdjlem  47465  ormklocald  47886  cjnpoly  47939  sinnpoly  47941  sqrtrrnpoly  47942  sqrtnegnre  48377  fsummmodsnunz  48453  flsqrt5  48679  bits0ALTV  48777  mogoldbblem  48818  sgoldbeven3prm  48881  nnsum3primes4  48886  isubgr0uhgr  48971  ushggricedg  49025  2zrngnmlid  49352  2zrngnmrid  49353  mpoexxg2  49450  lco0  49539  zlmodzxzldeplem3  49614  0dig1  49721  naryfvalel  49742  ackvalsuc0val  49799  iinxp  49941  0funclem  50194  aacllem  50939