Theorem mpan2 697

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 693	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mpanr12  711  mp3an23  1461  elvd  3437  elabg  3614  eueq2  3651  sbcgf  3793  sbcralg  3806  csbconstgf  3849  sbcnestgw  4351  csbnestgw  4352  sbcnestg  4356  csbnestg  4357  csbnest1g  4360  iinexg  5276  eusv2nf  5324  reusv2lem5  5331  nnullss  5401  xpss1  5637  xpiindi  5777  reldm0  5870  elrnmpt1s  5901  resdm  5978  eliniseg  6046  trinxp  6075  ssrnres  6129  cnveq0  6148  coi2  6215  relrelss  6224  cnviin  6237  elpred  6269  onelssex  6359  ord0eln0  6366  funcnvres  6563  funimaex  6573  fnresin1  6610  fnresin2  6611  fresin  6696  ssimaex  6912  fvmpt  6935  fvmptnf  6958  fvimacnvALT  6998  dff3  7041  fsn  7077  fsn2  7078  funop  7092  fvrnressn  7104  fnsnbg  7108  fninfp  7118  fndifnfp  7120  fnnfpeq0  7122  fprb  7138  elabrex  7186  elabrexg  7187  f1elima  7207  f1ofvswap  7250  fliftel1  7254  f1owe  7297  sorpssuni  7675  sorpssint  7676  eldifpw  7711  ordeleqon  7725  ordsson  7726  ssnlim  7826  abrexexg  7903  tposfun  8182  tpostpos2  8187  fpr3g  8225  wfr3g  8259  tfrlem10  8316  tfrlem12  8318  tfr3  8328  seqomlem1  8379  seqomlem2  8380  seqomlem4  8382  ondif2  8427  oa0  8441  om0  8442  oa1suc  8456  om1  8467  oe1  8469  oe1m  8470  omass  8505  om2  8511  oeoalem  8522  oeoelem  8524  nnmsucr  8551  nnm1  8578  nnm2  8579  naddrid  8609  naddlid  8610  ecelqs  8704  xpider  8725  mapdm0  8779  fvdiagfn  8829  ixpsnf1o  8876  xp1en  8991  undom  8993  sbthlem7  9021  domunsn  9055  xpmapenlem  9072  infensuc  9083  findcard2d  9091  diffi  9099  cnvfi  9100  enreffi  9107  snnen2o  9145  1sdom2dom  9154  infi  9170  finresfin  9172  unblem1  9192  unblem2  9193  unblem3  9194  unblem4  9195  isfinite2  9198  infn0ALT  9203  unfilem1  9205  unfilem2  9206  unfir  9208  fofinf1o  9232  cnvfiALT  9239  mptfi  9251  finsschain  9259  imafi2  9261  marypha2  9342  inf0  9533  trcl  9640  frr3g  9671  r1rankidb  9719  snwf  9724  unwf  9725  uniwf  9734  rankval3b  9741  rankr1a  9751  rankxplim3  9796  scott0  9801  djueq1  9820  card1  9883  pm54.43  9916  infxpenc2  9935  dfac8clem  9945  alephsuc2  9993  alephle  10001  cardaleph  10002  dfac12lem2  10058  undjudom  10081  djudom1  10096  pwdju1  10104  nnadju  10111  ackbij1lem18  10149  cflem  10158  cflemOLD  10159  cflecard  10166  cfeq0  10169  cfslb  10179  cfsmolem  10183  cfcoflem  10185  cfidm  10188  isfin4p1  10228  fin23lem12  10244  fin23lem16  10248  fin23lem28  10253  fin23lem38  10262  fin23lem41  10265  fin1a2lem7  10319  fin1a2lem12  10324  fin1a2lem13  10325  hsmexlem8  10337  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  ac6num  10392  ttukeylem4  10425  ttukeylem7  10428  ttukey2g  10429  axdclem  10432  brdom3  10441  brdom5  10442  cardeq0  10465  unsnen  10466  konigthlem  10482  pwcfsdom  10497  canthp1lem1  10566  wunex2  10652  wuncval2  10661  eltsk2g  10665  ingru  10729  grutsk  10736  axgroth6  10742  mulidpi  10800  nlt1pi  10820  indpi  10821  pinq  10841  mulidnq  10877  1idpr  10943  prlem934  10947  0idsr  11011  1idsr  11012  00sr  11013  negexsr  11016  recexsrlem  11017  sqgt0sr  11020  ax1rid  11075  axcnre  11078  ne0gt0  11242  peano2cn  11309  peano2re  11310  00id  11312  mul02lem2  11314  mul01  11316  subid  11404  subid1  11405  negid  11432  negeq0  11439  peano2cnm  11451  peano2rem  11452  lt0neg1  11647  le0neg1  11649  relin01  11665  div2neg  11869  recgt0ii  12053  divgt0i2i  12062  ledivp1i  12072  ltdivp1i  12073  inelr  12140  indconst0  12162  indconst1  12163  peano5nni  12168  peano2nn  12177  nnge1  12196  nnne0  12202  times2  12304  addltmul  12404  nn0p1nn  12467  peano2nn0  12468  nn0lele2xi  12484  fcdmnn0supp  12485  fcdmnn0fsupp  12486  fcdmnn0suppg  12487  peano2z  12559  peano2zm  12561  suprzcl  12600  zeo  12606  eluzaddi  12810  uzwo  12852  uzwo2  12853  infssuzle  12872  infssuzcl  12873  zq  12895  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  rphalfcl  12962  zgt1rpn0n1  12976  ltpnf  13062  nltmnf  13071  pnfge  13072  nltpnft  13107  xlemnf  13110  qsqueeze  13144  xlt0neg1  13162  xle0neg1  13164  xaddpnf1  13169  xaddmnf1  13171  xaddrid  13184  xsubge0  13204  xmul01  13210  xmulneg1  13212  xmulpnf1  13217  xmulrid  13222  supxrbnd  13271  supxrgtmnf  13272  supxrre1  13273  supxrre2  13274  elioopnf  13387  elicopnf  13389  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  fzprval  13530  fz0add1fz1  13681  fzofzp1  13710  fzostep1  13732  injresinj  13737  flge0nn0  13770  flge1nn  13771  btwnzge0  13778  modfrac  13834  om2uzsuci  13901  axdc4uzlem  13936  ser1const  14011  exp0  14018  exp1  14020  expn1  14024  nn0sqcl  14042  sqval  14067  sqeq0  14073  resqcl  14077  zsqcl  14082  expubnd  14131  binom21  14172  expnbnd  14185  nn0opthlem2  14222  bcnn  14265  bcn2  14272  bcn2p1  14278  bcnm1  14280  hasheq0  14316  hashsng  14322  hashen1  14323  hashunsnggt  14347  hashin  14364  hashdif  14366  hashgt23el  14377  hashxplem  14386  hashf1lem2  14409  hash2pr  14422  hash2prde  14423  pr2pwpr  14432  hash3tr  14444  iswrd  14468  wrdval  14469  hashwrdn  14500  ccatval2  14531  ccatrid  14541  eqs1  14566  s111  14569  ccatws1len  14574  repsw0  14730  repsw1  14736  cshw0  14747  wwlktovf  14909  relexpsucnnl  14983  reim0  15071  imval2  15104  cjne0  15116  abssq  15259  max0add  15263  abs2dif  15286  rddif  15294  absrdbnd  15295  rexuz3  15302  isershft  15617  isercolllem2  15619  isercoll  15621  fsum  15673  fsumadd  15693  fsumsplitsnun  15708  bcxmas  15791  infcvgaux2i  15814  fprod  15897  risefac0  15983  fallfac0  15984  risefac1  15989  fallfac1  15990  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  efi4p  16095  resin4p  16096  recos4p  16097  sinbnd  16138  cosbnd  16139  rpnnen2lem8  16179  rpnnen2lem12  16183  cnso  16205  dvdsmul2  16238  dvdslelem  16269  odd2np1lem  16300  mod2eq1n2dvds  16307  divalglem0  16353  divalglem1  16354  divalglem4  16356  divalglem5  16357  divalglem8  16360  flodddiv4  16375  bits0  16388  bitsp1o  16393  bitsf1  16406  sadadd2lem2  16410  gcd1  16488  lcm0val  16554  dvdslcm  16558  lcmeq0  16560  lcmgcd  16567  lcm1  16570  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  prm2orodd  16651  phiprm  16738  pc0  16816  pcdvdstr  16838  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  hashbc0  16967  setsval  17128  fsets  17130  setsres  17139  ressinbas  17206  ressress  17208  elrestr  17382  pwssnf1o  17453  xpsfrnel  17517  xpscf  17520  ismred2  17556  submre  17558  mreacs  17615  oppchomfval  17671  brssc  17772  isssc  17778  yonedalem4c  18234  oduleval  18246  isprs  18253  oduclatb  18464  chninf  18592  gsumval2a  18644  smndex1n0mnd  18874  mulg1  19048  mulgnegnn  19051  isghmOLD  19182  ghmghmrn  19201  cntrnsg  19310  oppgplusfval  19314  pgrpsubgsymg  19375  psgneldm2i  19471  efgrelexlemb  19716  frgp0  19726  frgpmhm  19731  vrgpf  19734  cntrcmnd  19808  cntrabl  19809  cygctb  19858  dprd0  19999  dprd2da  20010  mgpplusg  20116  opprmulfval  20310  subrngint  20532  subrgint  20567  lsp0  20999  rlmval2  21182  cncrng  21368  cnfld1  21372  zringcyg  21444  mulgrhm2  21453  zlmsca  21495  fermltlchr  21504  chrnzr  21505  zrhpsgnelbas  21569  ocvz  21653  cssincl  21663  css0  21664  css1  21665  frlmip  21753  fczpsrbag  21896  ply1idvr1OLD  22281  evls1rhmlem  22307  evl1fval1lem  22316  marrepeval  22546  decpmatid  22753  0opn  22887  topopn  22889  basdif0  22936  tgval  22938  isopn2  23015  0cld  23021  ntropn  23032  ntrval2  23034  ntrdif  23035  clsdif  23036  cmclsopn  23045  ntrtop  23053  ntr0  23064  mretopd  23075  neips  23096  neiptopnei  23115  maxlp  23130  isperf2  23135  rest0  23152  iocpnfordt  23198  icomnfordt  23199  mnfnei  23204  refref  23496  unisngl  23510  1stckgen  23537  ptbasfi  23564  pthaus  23621  fbssfi  23820  isfil2  23839  ssfg  23855  filconn  23866  fbasrn  23867  filufint  23903  imaelfm  23934  fmfnfmlem4  23940  fclsfnflim  24010  alexsubALTlem3  24032  alexsubALTlem4  24033  ustfilxp  24196  ustuqtop2  24225  ustuqtop4  24227  utopsnneiplem  24230  utopsnnei  24232  utop2nei  24233  cfiluweak  24277  neipcfilu  24278  xmetres  24347  metres  24348  mopnex  24502  prdsms  24514  metucn  24554  tngds  24631  tngngp3  24639  nmoge0  24704  cnfldnm  24761  tgioo  24779  xrtgioo  24790  xrsmopn  24796  negcncf  24907  phtpy01  24970  pco0  24999  tcphtopn  25211  tchnmfval  25213  caussi  25282  rrxip  25375  minveclem3b  25413  ovolfioo  25452  ovolficc  25453  ovolfsf  25456  ovolctb  25475  ovolctb2  25477  ovolfiniun  25486  ovoliun2  25491  ovolshftlem1  25494  ovolscalem1  25498  ovolicopnf  25509  iunmbl2  25542  uniioombllem2  25568  opnmblALT  25588  ismbf  25613  mbfinf  25650  0plef  25657  itg1climres  25699  itg2cnlem1  25746  iblitg  25753  ibl0  25772  itgcn  25830  cnlimc  25873  dvfre  25936  dvnfre  25937  dveflem  25964  dvef  25965  dvlipcn  25979  lhop2  26000  itgsubstlem  26033  deg1val  26079  ply1rem  26149  coefv0  26231  plyrecj  26264  vieta1lem2  26295  aannenlem1  26312  aaliou2b  26325  ulmval  26363  ulmpm  26366  ulmdvlem1  26383  mtest  26387  efcn  26426  sin2pim  26467  cos2pim  26468  sinmpi  26469  cosmpi  26470  sinppi  26471  cosppi  26472  efimpi  26473  sincosq1lem  26479  sincosq2sgn  26481  sincosq3sgn  26482  sincosq4sgn  26483  sinq12gt0  26489  sinq34lt0t  26491  sincosq1eq  26494  abssinper  26503  efif1o  26528  loglt1b  26616  relogcn  26620  ellogdm  26621  efopn  26640  cxp0  26652  cxp1  26653  cxpsqrt  26685  logsqrt  26686  logb1  26751  atandm3  26860  atanbnd  26908  atancn  26918  leibpi  26924  efrlim  26951  logdifbnd  26975  vmaprm  27098  ppip1le  27142  ppieq0  27157  prmorcht  27159  ppiublem1  27183  ppiub  27185  chpeq0  27189  chtub  27193  fsumvma  27194  pclogsum  27196  chpval2  27199  dchrresb  27240  dchrptlem1  27245  lgs0  27291  lgs2  27295  lgsdir2lem2  27307  lgsdir2lem4  27309  lgsdchrval  27335  lgsdchr  27336  lgseisenlem2  27357  2lgslem1c  27374  2lgsoddprmlem2  27390  addsq2nreurex  27425  dirith2  27509  selberg2lem  27531  qabvle  27606  qabvexp  27607  ostth  27620  noextendseq  27649  noetasuplem4  27718  noetainflem4  27722  cutsun12  27800  madebdayim  27898  bdayiun  27925  addsrid  27974  addsfo  27993  peano2no  27994  negscl  28046  subsfo  28075  subsid1  28078  muls01  28122  mulsrid  28123  divs1  28214  recsex  28229  abssnid  28253  peano2ons  28290  noseqp1  28301  noseqind  28302  peano2nns  28360  n0fincut  28365  n0lts1e0  28378  dfnns2  28382  oldfib  28387  elzs2  28409  elnnzs  28411  elznns  28412  zsoring  28419  n0seo  28431  exps0  28437  exps1  28438  bdaypw2n0bndlem  28473  bdayfin  28497  istrkg2ld  28546  istrkg3ld  28547  ttgval  28961  brbtwn  28986  colinearalglem4  28996  upgr0eop  29201  uspgrushgr  29264  usgruspgr  29267  usgr0eop  29333  0grsubgr  29365  uspgrloopvtx  29602  umgr2v2evtx  29608  usgr0edg0rusgr  29662  rgrusgrprc  29676  wlkvtxiedg  29711  pthdivtx  29813  usgr2pthlem  29849  wlkswwlksf1o  29965  wwlksext2clwwlk  30145  konigsbergssiedgw  30338  frgrncvvdeqlem7  30393  2clwwlk2  30436  ex-po  30523  pliguhgr  30575  nvnd  30777  ipval2lem3  30794  ipval2  30796  ipidsq  30799  dipcj  30803  dip0r  30806  nmlnogt0  30886  blocni  30894  ipasslem2  30921  ipasslem8  30926  ipasslem9  30927  ajval  30950  ubthlem1  30959  hvaddlid  31112  hvsub0  31165  hi02  31186  hlimi  31277  isch2  31312  chlimi  31323  chsupunss  31433  shsupunss  31435  chlejb1i  31565  h1dei  31639  h1de2ci  31645  spanunsni  31668  pjoml2i  31674  pjorthi  31758  mayete3i  31817  hosubid1  31887  nmopge0  32000  nmfnge0  32016  adj1  32022  adjeq  32024  lnop0  32055  lnopmi  32089  nmophmi  32120  cnlnadjlem5  32160  cnlnadjeui  32166  unierri  32193  leoprf2  32216  leopnmid  32227  nmopleid  32228  hstles  32320  hst0  32322  strlem3a  32341  dmdbr2  32392  mdsl1i  32410  mdsl2i  32411  mdsl2bi  32412  cvmdi  32413  mdslmd1lem1  32414  mdslmd1lem2  32415  mdslmd1i  32418  mdslmd2i  32419  csmdsymi  32423  mdexchi  32424  superpos  32443  atomli  32471  atordi  32473  chirredlem1  32479  chirredlem2  32480  atcvat4i  32486  atabsi  32490  mdsymlem1  32492  mdsymlem5  32496  mdsymlem6  32497  sumdmdii  32504  dmdbr5ati  32511  dmdbr6ati  32512  mddmdin0i  32520  cdj3lem2  32524  unidifsnel  32623  unidifsnne  32624  xppreima  32737  abfmpunirn  32744  abfmpel  32747  aciunf1lem  32754  fgreu  32763  padct  32810  fpwrelmapffslem  32824  fpwrelmap  32825  xrge0infss  32852  xrdifh  32872  pfx1s2  33018  clatp0cl  33055  clatp1cl  33056  cntrcrng  33162  cycpmco2lem4  33210  rmfsupp2  33319  1fldgenq  33406  resvval  33412  rearchi  33429  qusxpid  33446  opprabs  33565  zringfrac  33637  psrbasfsupp  33695  0mplrim  33698  rlmdim  33794  constrfiss  33935  2sqr3minply  33964  locfinreflem  34024  locfinref  34025  ordtconnlem1  34108  rge0scvg  34133  lmxrge0  34136  qqh0  34168  qqh1  34169  rrh0  34199  zrhre  34203  esumcst  34247  esumfzf  34253  esumfsupre  34255  hasheuni  34269  sgon  34308  dmvlsiga  34313  sigainb  34320  measval  34382  ismeas  34383  sxbrsigalem0  34455  omssubadd  34484  carsggect  34502  eulerpartlemmf  34559  eulerpartlemgs2  34564  eulerpartlemn  34565  rrvsum  34638  ballotlem2  34673  ballotlemfcc  34678  ballotlem4  34683  signsplypnf  34734  signsply0  34735  signsw0glem  34737  signswrid  34742  signlem0  34771  signshf  34772  bnj535  35072  bnj580  35095  bnj907  35149  bnj1253  35199  funen1cnv  35269  rankval4b  35281  fineqvnttrclse  35305  noinfepfnregs  35313  onvf1odlem1  35331  onvf1od  35335  loop1cycl  35365  ptpconn  35461  cvmsss2  35502  cvmlift2lem12  35542  cvmlift2lem13  35543  cvmliftphtlem  35545  cvmliftpht  35546  fmlafvel  35613  mppsthm  35807  bcneg1  35964  fv1stcnv  36005  fv2ndcnv  36006  wlimeq1  36046  imagesset  36181  altopeq1  36191  brcolinear2  36286  cldbnd  36554  ivthALT  36563  refssfne  36586  ontgval  36659  onint1  36677  ttcid  36720  ttcss  36726  ttcss2  36727  ttcsnexg  36748  ttcwf  36752  dfttc4lem2  36757  ttc0el  36763  axc11n11r  37026  bj-pm11.53a  37113  bj-bm1.3ii  37417  bj-restsn0  37443  bj-restsn10  37444  bj-restsnid  37445  bj-rest10  37446  bj-rest0  37451  bj-inftyexpiinv  37568  bj-inftyexpidisj  37570  taupilem1  37681  irrdiff  37686  qdiff  37687  f1omptsnlem  37698  mptsnunlem  37700  topdifinffinlem  37709  inunissunidif  37737  rdgssun  37740  exrecfnlem  37741  exrecfnpw  37743  finixpnum  37972  tan2h  37979  matunitlindflem2  37984  ptrest  37986  poimirlem22  38009  poimirlem25  38012  mblfinlem1  38024  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  ftc1anclem5  38064  ftc1anclem8  38067  dvasin  38071  dvacos  38072  sdclem2  38109  totbndbnd  38156  heibor1lem  38176  heiborlem7  38184  bfplem1  38189  prnc  38434  brxrn  38750  ecxrn2  38775  dfpeters2  39341  riotasv  39451  glbconN  39869  atpointN  40235  polsubN  40399  pol0N  40401  pol1N  40402  2polvalN  40406  2polssN  40407  3polN  40408  pcl0N  40414  2pmaplubN  40418  pnonsingN  40425  polsubclN  40444  cdlemefs32sn1aw  40906  cdleme43fsv1snlem  40912  cdleme41sn3a  40925  cdleme32a  40933  cdleme40m  40959  cdleme40n  40960  cdleme42b  40970  istendo  41252  cdlemk40  41409  cdlemkid  41428  dihvalcqpre  41727  facp2  42628  relt0neg1  42946  sn-nnne0  42950  frlmsnic  43026  prjspnerlem  43067  prjspnval2  43068  0prjspn  43078  3cubes  43139  mapfzcons1cl  43167  eldioph3b  43214  eldiophss  43223  0dioph  43227  vdioph  43228  eldioph4b  43256  eldioph4i  43257  rencldnfilem  43265  rmxy1  43367  rmxy0  43368  rmxm1  43379  rmym1  43380  monotoddzzfi  43387  wepwso  43488  aomclem6  43504  pwslnmlem0  43536  isnumbasabl  43551  areaquad  43661  onexlimgt  43688  oaabsb  43739  nadd1suc  43837  oe2  43850  safesnsupfidom1o  43861  onnoxp  43877  oa1cl  43891  finona1cl  43897  reabsifneg  44076  reabsifnneg  44079  relexp2  44121  eltrclrec  44124  elrtrclrec  44125  brtrclrec  44140  brrtrclrec  44141  relexpxpmin  44161  dftrcl3  44164  dfrtrcl3  44177  heeq1  44221  seff  44753  lhe4.4ex1a  44773  eelT0  45218  snssl  45273  sineq0ALT  45380  trfr  45406  xpwf  45408  dmwf  45409  rnwf  45410  modelaxreplem1  45422  modelaxreplem3  45424  0elaxnul  45427  prclaxpr  45429  uniclaxun  45430  wfac8prim  45446  permaxinf2lem  45456  elrnmpt1sf  45636  founiiun0  45637  supxrgere  45778  supxrgelem  45782  fmuldfeqlem1  46027  fmuldfeq  46028  climneg  46055  sumnnodd  46075  liminfltlem  46247  xlimpnfxnegmnf2  46301  addccncf2  46319  dvsinax  46356  stoweidlem18  46461  stoweidlem19  46462  stoweidlem22  46465  stoweidlem34  46477  stoweidlem40  46483  stoweidlem41  46484  stoweidlem55  46498  stoweidlem59  46502  dirker2re  46535  dirkerdenne0  46536  fourierdlem48  46597  fourierdlem49  46598  fourierdlem70  46619  fourierdlem71  46620  fourierdlem104  46653  fourierdlem112  46661  fouriersw  46674  etransclem46  46723  etransclem48  46725  nnfoctbdjlem  46898  ormklocald  47319  natlocalincr  47321  cjnpoly  47352  sinnpoly  47354  sqrtnegnre  47770  fsummmodsnunz  47846  flsqrt5  48072  bits0ALTV  48170  mogoldbblem  48211  sgoldbeven3prm  48274  nnsum3primes4  48279  isubgr0uhgr  48364  ushggricedg  48418  2zrngnmlid  48746  2zrngnmrid  48747  mpoexxg2  48829  lco0  48918  zlmodzxzldeplem3  48993  0dig1  49100  naryfvalel  49121  ackvalsuc0val  49178  iinxp  49321  0funclem  49576  aacllem  50291