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  3821  csbconstgf  3865  sbcnestgw  4380  csbnestgw  4381  sbcnestg  4385  csbnestg  4386  csbnest1g  4389  ssex  5281  iinexg  5308  eusv2nf  5356  reusv2lem5  5363  nnullss  5429  xpss1  5669  xpiindi  5812  reldm0  5910  elrnmpt1s  5941  resdm  6016  eliniseg  6093  trinxp  6120  ssrnres  6171  cnveq0  6192  coi2  6267  relrelss  6277  relresfld  6280  cnviin  6291  elpred  6323  onelssex  6414  ord0eln0  6421  funcnvres  6621  funimaex  6630  fnresin1  6667  fnresin2  6668  fresin  6754  ssimaex  6973  fvmpt  6996  fvmptnf  7019  fvimacnvALT  7059  dff3  7103  fsn  7139  fsn2  7140  funop  7156  fvrnressn  7168  fnsnbg  7172  fninfp  7181  fndifnfp  7183  fnnfpeq0  7185  fprb  7201  elabrex  7248  elabrexg  7249  f1elima  7269  f1ofvswap  7316  fliftel1  7320  f1owe  7363  f1oweOLD  7364  sorpssuni  7750  sorpssint  7751  eldifpw  7784  ordeleqon  7798  ordsson  7799  ssnlim  7899  abrexexg  7975  tposfun  8264  tpostpos2  8269  fpr3g  8308  wfr3g  8342  tfrlem10  8400  tfrlem12  8402  tfr3  8412  seqomlem1  8465  seqomlem2  8466  seqomlem4  8468  ondif2  8515  oa0  8529  om0  8530  oa1suc  8544  om1  8555  oe1  8557  oe1m  8558  omass  8593  om2  8599  oeoalem  8610  oeoelem  8612  nnmsucr  8639  nnm1  8666  nnm2  8667  naddrid  8698  naddlid  8699  ecelqs  8793  xpider  8814  mapdm0  8867  fvdiagfn  8924  ixpsnf1o  8971  funen1cnv  9061  xp1en  9087  undom  9089  sbthlem7  9117  domunsn  9151  xpmapenlem  9168  infensuc  9179  findcard2d  9187  diffi  9195  cnvfi  9196  enreffi  9203  snnen2o  9241  1sdom2dom  9250  infi  9266  finresfin  9268  unblem1  9289  unblem2  9290  unblem3  9291  unblem4  9292  isfinite2  9295  infn0ALT  9300  unfilem1  9302  unfilem2  9303  unfir  9305  fofinf1o  9326  cnvfiALT  9333  mptfi  9345  finsschain  9353  imafi2  9355  marypha2  9436  inf0  9627  trcl  9734  frr3g  9765  r1rankidb  9817  snwf  9822  unwf  9823  uniwf  9833  rankval3b  9841  rankr1a  9853  rankval4b  9885  rankxplim3  9903  hfuni  9929  scott0b  9942  scott0OLD  9943  djueq1  9991  card1  10054  pm54.43  10087  infxpenc2  10106  dfac8clem  10116  alephsuc2  10164  alephle  10172  cardaleph  10173  dfac12lem2  10228  undjudom  10251  djudom1  10266  pwdju1  10274  nnadju  10281  ackbij1lem18  10319  cflem  10328  cflecard  10335  cfeq0  10339  cfslb  10349  cfsmolem  10353  cfcoflem  10355  cfidm  10358  isfin4p1  10398  fin23lem12  10414  fin23lem16  10418  fin23lem28  10423  fin23lem38  10432  fin23lem41  10435  fin1a2lem7  10489  fin1a2lem12  10494  fin1a2lem13  10495  hsmexlem8  10507  axcc2lem  10519  axcc3  10521  domtriomlem  10525  axdc3lem2  10534  axdc3lem4  10536  axdc4lem  10538  axcclem  10540  ac6num  10562  ttukeylem4  10595  ttukeylem7  10598  ttukey2g  10599  axdclem  10602  brdom3  10612  brdom5  10613  imadomnum  10619  cardeq0  10641  unsnen  10642  konigthlem  10658  pwcfsdom  10673  canthp1lem1  10742  wunex2  10828  wuncval2  10837  eltsk2g  10841  ingru  10905  grutsk  10912  axgroth6  10918  mulidpi  10976  nlt1pi  10996  indpi  10997  pinq  11017  mulidnq  11053  1idpr  11119  prlem934  11123  0idsr  11187  1idsr  11188  00sr  11189  negexsr  11192  recexsrlem  11193  sqgt0sr  11196  ax1rid  11251  axcnre  11254  ne0gt0  11420  peano2cn  11487  peano2re  11488  00id  11490  mul02lem2  11492  mul01  11494  subid  11582  subid1  11583  negid  11610  negeq0  11617  peano2cnm  11629  peano2rem  11630  lt0neg1  11827  le0neg1  11829  relin01  11845  div2neg  12045  recgt0ii  12228  divgt0i2i  12237  ledivp1i  12247  ltdivp1i  12248  inelr  12315  indconst0  12337  indconst1  12338  peano5nni  12343  peano2nn  12352  nnge1  12371  nnne0  12377  times2  12484  addltmul  12587  nn0p1nn  12650  peano2nn0  12651  nn0lele2xi  12667  fcdmnn0supp  12668  fcdmnn0fsupp  12669  fcdmnn0suppg  12670  peano2z  12742  peano2zm  12744  suprzcl  12784  zeo  12790  eluzaddi  13001  uzwo  13043  uzwo2  13044  infssuzle  13063  infssuzcl  13064  zq  13086  rpnnen1lem1  13111  rpnnen1lem3  13112  rpnnen1lem5  13114  rphalfcl  13154  zgt1rpn0n1  13168  ltpnf  13254  nltmnf  13263  pnfge  13264  nltpnft  13299  xlemnf  13302  qsqueeze  13336  xlt0neg1  13354  xle0neg1  13356  xaddpnf1  13361  xaddmnf1  13363  xaddrid  13376  xsubge0  13396  xmul01  13402  xmulneg1  13404  xmulpnf1  13409  xmulrid  13414  supxrbnd  13463  supxrgtmnf  13464  supxrre1  13465  supxrre2  13466  elioopnf  13579  elicopnf  13581  iccshftri  13623  iccshftli  13625  iccdili  13627  icccntri  13629  fzprval  13724  fz0add1fz1  13875  fzofzp1  13904  fzostep1  13926  injresinj  13931  flge0nn0  13965  flge1nn  13966  btwnzge0  13973  modfrac  14029  om2uzsuci  14096  axdc4uzlem  14131  ser1const  14206  exp0  14213  exp1  14215  expn1  14219  nn0sqcl  14237  sqval  14262  sqeq0  14268  resqcl  14272  zsqcl  14277  expubnd  14326  binom21  14368  expnbnd  14381  nn0opthlem2  14418  bcnn  14461  bcn2  14468  bcn2p1  14474  bcnm1  14476  hasheq0  14512  hashsng  14518  hashen1  14519  hashunsnggt  14543  hashin  14561  hashdif  14563  hashgt23el  14574  hashxplem  14583  hashf1lem2  14606  hash2pr  14619  hash2prde  14620  pr2pwpr  14629  hash3tr  14641  iswrd  14665  wrdval  14666  hashwrdn  14697  ccatval2  14728  ccatrid  14738  eqs1  14766  s111  14769  ccatws1len  14774  repsw0  14934  repsw1  14940  cshw0  14951  wwlktovf  15116  relexpsucnnl  15190  reim0  15292  imval2  15325  cjne0  15337  abssq  15480  max0add  15484  abs2dif  15507  rddif  15515  absrdbnd  15516  rexuz3  15523  isershft  15838  isercolllem2  15840  isercoll  15842  fsum  15893  fsumadd  15913  fsumsplitsnun  15928  bcxmas  16011  infcvgaux2i  16034  fprod  16115  risefac0  16200  fallfac0  16201  risefac1  16206  fallfac1  16207  bpoly2  16230  bpoly3  16231  bpoly4  16232  fsumcube  16233  efi4p  16312  resin4p  16313  recos4p  16314  sinbnd  16355  cosbnd  16356  rpnnen2lem8  16396  rpnnen2lem12  16400  cnso  16422  dvdsmul2  16455  dvdslelem  16486  odd2np1lem  16517  mod2eq1n2dvds  16524  divalglem0  16570  divalglem1  16571  divalglem4  16573  divalglem5  16574  divalglem8  16577  flodddiv4  16592  bits0  16605  bitsp1o  16610  bitsf1  16623  sadadd2lem2  16627  gcd1  16708  lcm0val  16776  dvdslcm  16780  lcmeq0  16782  lcmgcd  16789  lcm1  16792  lcmfunsnlem2lem2  16821  lcmfunsnlem2  16822  prm2orodd  16873  phiprm  16961  pc0  17039  pcdvdstr  17061  vdwlem2  17167  vdwlem6  17171  vdwlem8  17173  hashbc0  17190  setsval  17352  fsets  17354  setsres  17363  ressinbas  17430  ressress  17432  elrestr  17606  pwssnf1o  17677  xpsfrnel  17741  xpscf  17744  ismred2  17780  submre  17782  mreacs  17839  oppchomfval  17895  brssc  17996  isssc  18002  yonedalem4c  18458  oduleval  18470  isprs  18477  oduclatb  18688  chninf  18816  gsumval2a  18881  smndex1n0mnd  19118  mulg1  19298  mulgnegnn  19301  qusxpid  19402  ghmghmrn  19456  cntrnsg  19565  oppgplusfval  19569  pgrpsubgsymg  19630  psgneldm2i  19726  efgrelexlemb  19971  frgp0  19981  frgpmhm  19986  vrgpf  19989  cntrcmnd  20063  cntrabl  20064  cygctb  20113  dprd0  20254  dprd2da  20265  mgpplusg  20371  opprmulfval  20576  subrngint  20819  subrgint  20854  lsp0  21291  rlmval2  21474  cncrng  21706  cnfld1  21710  zringcyg  21782  mulgrhm2  21791  zlmsca  21833  fermltlchr  21842  chrnzr  21843  zrhpsgnelbas  21907  ocvz  21991  cssincl  22001  css0  22002  css1  22003  frlmip  22091  fczpsrbag  22236  evls1rhmlem  22646  evl1fval1lem  22655  marrepeval  22885  matunitlindflem2  23002  decpmatid  23095  0opn  23229  topopn  23231  basdif0  23278  tgval  23280  isopn2  23357  0cld  23363  ntropn  23374  ntrval2  23376  ntrdif  23377  clsdif  23378  cmclsopn  23387  ntrtop  23395  ntr0  23406  mretopd  23417  neips  23438  neiptopnei  23457  maxlp  23472  isperf2  23477  rest0  23494  iocpnfordt  23540  icomnfordt  23541  mnfnei  23546  refref  23839  unisngl  23853  1stckgen  23880  ptbasfi  23907  pthaus  23964  fbssfi  24163  isfil2  24182  ssfg  24198  filconn  24209  fbasrn  24210  filufint  24246  imaelfm  24277  fmfnfmlem4  24283  fclsfnflim  24353  alexsubALTlem3  24375  alexsubALTlem4  24376  ustfilxp  24539  ustuqtop2  24568  ustuqtop4  24570  utopsnneiplem  24573  utopsnnei  24575  utop2nei  24576  cfiluweak  24620  neipcfilu  24621  xmetres  24690  metres  24691  mopnex  24845  prdsms  24857  metucn  24897  tngds  24974  tngngp3  24982  nmoge0  25047  cnfldnm  25104  tgioo  25122  xrtgioo  25133  xrsmopn  25139  negcncf  25250  phtpy01  25313  pco0  25342  tcphtopn  25554  tchnmfval  25556  caussi  25625  rrxip  25718  minveclem3b  25756  ovolfioo  25795  ovolficc  25796  ovolfsf  25799  ovolctb  25818  ovolctb2  25820  ovolfiniun  25829  ovoliun2  25834  ovolshftlem1  25837  ovolscalem1  25841  ovolicopnf  25852  iunmbl2  25885  uniioombllem2  25911  opnmblALT  25931  ismbf  25956  mbfinf  25993  0plef  26000  itg1climres  26042  itg2cnlem1  26089  iblitg  26096  ibl0  26114  itgcn  26172  cnlimc  26215  dvfre  26278  dvnfre  26279  dveflem  26306  dvef  26307  dvlipcn  26321  lhop2  26342  itgsubstlem  26375  deg1val  26421  ply1rem  26491  coefv0  26574  plyrecj  26605  rnplynfin  26637  vieta1lem2  26641  aannenlem1  26662  aaliou2b  26675  ulmval  26714  ulmpm  26717  ulmdvlem1  26734  mtest  26738  efcn  26777  sin2pim  26821  cos2pim  26822  sinmpi  26823  cosmpi  26824  sinppi  26825  cosppi  26826  efimpi  26827  sincosq1lem  26833  sincosq2sgn  26835  sincosq3sgn  26836  sincosq4sgn  26837  sinq12gt0  26843  sinq34lt0t  26845  sincosq1eq  26848  abssinper  26856  efif1o  26881  loglt1b  26969  relogcn  26973  ellogdm  26974  efopn  26993  cxp0  27005  cxp1  27006  cxpsqrt  27038  logsqrt  27039  logb1  27104  atandm3  27213  atanbnd  27261  atancn  27271  leibpi  27277  efrlim  27304  logdifbnd  27328  vmaprm  27451  ppip1le  27495  ppieq0  27510  prmorcht  27512  ppiublem1  27536  ppiub  27538  chpeq0  27542  chtub  27546  fsumvma  27547  pclogsum  27549  chpval2  27552  dchrresb  27593  dchrptlem1  27598  lgs0  27644  lgs2  27648  lgsdir2lem2  27660  lgsdir2lem4  27662  lgsdchrval  27688  lgsdchr  27689  lgseisenlem2  27710  2lgslem1c  27727  2lgsoddprmlem2  27743  addsq2nreurex  27778  dirith2  27862  selberg2lem  27884  qabvle  27959  qabvexp  27960  ostth  27973  noextendseq  28031  noetasuplem4  28100  noetainflem4  28104  cutsun12  28183  madebdayim  28281  bdayiun  28308  addsrid  28357  addsfo  28376  peano2no  28377  negscl  28429  subsfo  28458  subsid1  28461  muls01  28505  mulsrid  28506  divs1  28597  recsex  28612  abssnid  28636  peano2ons  28673  noseqp1  28684  noseqind  28685  peano2nns  28743  n0fincut  28748  n0lts1e0  28761  dfnns2  28765  oldfib  28770  elzs2  28792  elnnzs  28794  elznns  28795  zsoring  28802  n0seo  28814  exps0  28820  exps1  28821  bdaypw2n0bndlem  28856  bdayfin  28880  istrkg2ld  28929  istrkg3ld  28930  ttgval  29459  brbtwn  29484  colinearalglem4  29494  upgr0eop  29699  uspgrushgr  29765  usgruspgr  29768  usgr0eop  29834  0grsubgr  29866  uspgrloopvtx  30103  umgr2v2evtx  30109  usgr0edg0rusgr  30163  rgrusgrprc  30177  wlkvtxiedg  30212  pthdivtx  30319  usgr2pthlem  30356  wlkswwlksf1o  30475  wwlksext2clwwlk  30655  loop1cycl  30751  konigsbergssiedgw  30858  frgrncvvdeqlem7  30913  2clwwlk2  30956  ex-po  31043  pliguhgr  31095  nvnd  31297  ipval2lem3  31314  ipval2  31316  ipidsq  31319  dipcj  31323  dip0r  31326  nmlnogt0  31406  blocni  31414  ipasslem2  31441  ipasslem8  31446  ipasslem9  31447  ajval  31470  ubthlem1  31479  hvaddlid  31632  hvsub0  31685  hi02  31706  hlimi  31797  isch2  31832  chlimi  31843  chsupunss  31953  shsupunss  31955  chlejb1i  32085  h1dei  32159  h1de2ci  32165  spanunsni  32188  pjoml2i  32194  pjorthi  32278  mayete3i  32337  hosubid1  32407  nmopge0  32520  nmfnge0  32536  adj1  32542  adjeq  32544  lnop0  32575  lnopmi  32609  nmophmi  32640  cnlnadjlem5  32680  cnlnadjeui  32686  unierri  32713  leoprf2  32736  leopnmid  32747  nmopleid  32748  hstles  32840  hst0  32842  strlem3a  32861  dmdbr2  32912  mdsl1i  32930  mdsl2i  32931  mdsl2bi  32932  cvmdi  32933  mdslmd1lem1  32934  mdslmd1lem2  32935  mdslmd1i  32938  mdslmd2i  32939  csmdsymi  32943  mdexchi  32944  superpos  32963  atomli  32991  atordi  32993  chirredlem1  32999  chirredlem2  33000  atcvat4i  33006  atabsi  33010  mdsymlem1  33012  mdsymlem5  33016  mdsymlem6  33017  sumdmdii  33024  dmdbr5ati  33031  dmdbr6ati  33032  mddmdin0i  33040  cdj3lem2  33044  unidifsnel  33180  unidifsnne  33181  xppreima  33288  abfmpunirn  33295  abfmpel  33298  aciunf1lem  33305  fgreu  33314  padct  33359  fpwrelmapffslem  33372  fpwrelmap  33373  xrge0infss  33400  xrdifh  33420  pfx1s2  33554  clatp0cl  33585  clatp1cl  33586  cntrcrng  33690  cycpmco2lem4  33738  rmfsupp2  33846  1fldgenq  33932  resvval  33938  rearchi  33955  opprabs  34054  zringfrac  34134  psrbasfsupp  34191  0mplrim  34194  rlmdim  34290  constrfiss  34431  2sqr3minply  34460  locfinreflem  34520  locfinref  34521  ordtconnlem1  34604  rge0scvg  34629  lmxrge0  34632  qqh0  34664  qqh1  34665  rrh0  34695  zrhre  34699  esumcst  34743  esumfzf  34749  esumfsupre  34751  hasheuni  34765  sgon  34804  dmvlsiga  34809  sigainb  34817  measval  34879  ismeas  34880  sxbrsigalem0  34951  omssubadd  34980  carsggect  34998  eulerpartlemmf  35055  eulerpartlemgs2  35060  eulerpartlemn  35061  rrvsum  35134  ballotlem2  35169  ballotlemfcc  35174  ballotlem4  35179  signsplypnf  35227  signsply0  35228  signsw0glem  35230  signswrid  35235  signlem0  35264  signshf  35265  bnj535  35568  bnj580  35591  bnj907  35645  bnj1253  35695  rncardr1prc  35816  fineqvnttrclse  35850  noinfepfnregs  35858  onvf1odlem1  35952  onvf1od  35956  ptpconn  36086  cvmsss2  36127  cvmlift2lem12  36167  cvmlift2lem13  36168  cvmliftphtlem  36170  cvmliftpht  36171  fmlafvel  36238  mppsthm  36432  bcneg1  36595  fv1stcnv  36635  fv2ndcnv  36636  wlimeq1  36676  imagesset  36811  altopeq1  36822  brcolinear2  36917  nmulr0  37038  nmull0  37039  nmulrid  37040  cldbnd  37208  ivthALT  37217  refssfne  37240  ontgval  37313  onint1  37331  ttcid  37374  ttcss  37380  ttcss2  37381  ttcsnexg  37402  ttcwf  37406  dfttc4lem2  37411  ttc0el  37417  axc11n11r  37679  bj-pm11.53a  37766  bj-bm1.3ii  38085  bj-restsn0  38112  bj-restsn10  38113  bj-restsnid  38114  bj-rest10  38115  bj-rest0  38120  bj-inftyexpiinv  38236  bj-inftyexpidisj  38238  taupilem1  38349  irrdiff  38354  qdiff  38355  f1omptsnlem  38366  mptsnunlem  38368  topdifinffinlem  38377  inunissunidif  38405  rdgssun  38408  exrecfnlem  38409  exrecfnpw  38411  finixpnum  38635  tan2h  38642  ptrest  38644  poimirlem22  38667  poimirlem25  38670  mblfinlem1  38682  mblfinlem2  38683  mblfinlem3  38684  mblfinlem4  38685  ismblfin  38686  itg2addnclem  38696  itg2addnclem2  38697  itg2addnclem3  38698  itg2addnc  38699  itg2gt0cn  38700  ftc1anclem5  38722  ftc1anclem8  38725  dvasin  38729  dvacos  38730  sdclem2  38783  totbndbnd  38830  heibor1lem  38850  heiborlem7  38858  bfplem1  38863  prnc  39108  brxrn  39422  ecxrn2  39447  dfpeters2  40013  riotasv  40123  glbconN  40541  atpointN  40907  polsubN  41071  pol0N  41073  pol1N  41074  2polvalN  41078  2polssN  41079  3polN  41080  pcl0N  41086  2pmaplubN  41090  pnonsingN  41097  polsubclN  41116  cdlemefs32sn1aw  41578  cdleme43fsv1snlem  41584  cdleme41sn3a  41597  cdleme32a  41605  cdleme40m  41631  cdleme40n  41632  cdleme42b  41642  istendo  41924  cdlemk40  42081  cdlemkid  42100  dihvalcqpre  42399  facp2  43300  relt0neg1  43627  sn-nnne0  43631  frlmsnic  43711  prjspnerlem  43752  prjspnval2  43753  0prjspn  43771  3cubes  43807  mapfzcons1cl  43836  eldioph3b  43883  eldiophss  43892  0dioph  43896  vdioph  43897  eldioph4b  43925  eldioph4i  43926  rencldnfilem  43934  rmxy1  44036  rmxy0  44037  rmxm1  44048  rmym1  44049  monotoddzzfi  44056  wepwso  44157  aomclem6  44168  pwslnmlem0  44200  isnumbasabl  44215  areaquad  44325  onexlimgt  44352  oaabsb  44403  nadd1suc  44501  oe2  44514  safesnsupfidom1o  44525  onnoxp  44541  oa1cl  44555  finona1cl  44561  reabsifneg  44739  reabsifnneg  44742  relexp2  44784  eltrclrec  44787  elrtrclrec  44788  brtrclrec  44803  brrtrclrec  44804  relexpxpmin  44824  dftrcl3  44827  dfrtrcl3  44840  heeq1  44884  seff  45400  lhe4.4ex1a  45420  eelT0  45864  snssl  45919  sineq0ALT  46026  trfr  46059  xpwf  46061  dmwf  46062  rnwf  46063  modelaxreplem1  46075  modelaxreplem3  46077  0elaxnul  46080  prclaxpr  46082  uniclaxun  46083  wfac8prim  46099  permaxinf2lem  46109  hashnnsuc  46117  elrnmpt1sf  46311  founiiun0  46312  supxrgere  46452  supxrgelem  46456  fmuldfeqlem1  46701  fmuldfeq  46702  climneg  46729  sumnnodd  46749  liminfltlem  46921  xlimpnfxnegmnf2  46975  addccncf2  46993  dvsinax  47030  stoweidlem18  47135  stoweidlem19  47136  stoweidlem22  47139  stoweidlem34  47151  stoweidlem40  47157  stoweidlem41  47158  stoweidlem55  47172  stoweidlem59  47176  dirker2re  47209  dirkerdenne0  47210  fourierdlem48  47271  fourierdlem49  47272  fourierdlem70  47293  fourierdlem71  47294  fourierdlem104  47327  fourierdlem112  47335  fouriersw  47348  etransclem46  47397  etransclem48  47399  nnfoctbdjlem  47572  ormklocald  47993  cjnpoly  48046  sinnpoly  48048  sqrtrrnpoly  48049  sqrtnegnre  48484  fsummmodsnunz  48560  flsqrt5  48786  bits0ALTV  48884  mogoldbblem  48925  sgoldbeven3prm  48988  nnsum3primes4  48993  isubgr0uhgr  49078  ushggricedg  49132  2zrngnmlid  49459  2zrngnmrid  49460  mpoexxg2  49557  lco0  49646  zlmodzxzldeplem3  49721  0dig1  49828  naryfvalel  49849  ackvalsuc0val  49906  iinxp  50049  0funclem  50308  parswapprop  50884  aacllem  51121