Theorem mpan2 701

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpanr12  715  mp3an23  1473  elvd  3459  elabg  3634  eueq2  3671  sbcgf  3812  sbcralg  3825  csbconstgf  3868  sbcnestgw  4374  csbnestgw  4375  sbcnestg  4379  csbnestg  4380  csbnest1g  4383  iinexg  5301  eusv2nf  5349  reusv2lem5  5356  nnullss  5426  xpss1  5662  xpiindi  5803  reldm0  5900  elrnmpt1s  5931  resdm  6008  eliniseg  6079  trinxp  6108  ssrnres  6159  cnveq0  6179  coi2  6246  relrelss  6255  cnviin  6268  elpred  6300  onelssex  6390  ord0eln0  6397  funcnvres  6594  funimaex  6604  fnresin1  6641  fnresin2  6642  fresin  6728  ssimaex  6947  fvmpt  6970  fvmptnf  6993  fvimacnvALT  7033  dff3  7076  fsn  7112  fsn2  7113  funop  7127  fvrnressn  7139  fnsnbg  7143  fninfp  7153  fndifnfp  7155  fnnfpeq0  7157  fprb  7173  elabrex  7221  elabrexg  7222  f1elima  7242  f1ofvswap  7285  fliftel1  7289  f1owe  7332  sorpssuni  7710  sorpssint  7711  eldifpw  7746  ordeleqon  7760  ordsson  7761  ssnlim  7861  abrexexg  7937  tposfun  8216  tpostpos2  8221  fpr3g  8260  wfr3g  8294  tfrlem10  8352  tfrlem12  8354  tfr3  8364  seqomlem1  8415  seqomlem2  8416  seqomlem4  8418  ondif2  8465  oa0  8479  om0  8480  oa1suc  8494  om1  8505  oe1  8507  oe1m  8508  omass  8543  om2  8549  oeoalem  8560  oeoelem  8562  nnmsucr  8589  nnm1  8616  nnm2  8617  naddrid  8648  naddlid  8649  ecelqs  8743  xpider  8764  mapdm0  8817  fvdiagfn  8867  ixpsnf1o  8914  xp1en  9029  undom  9031  sbthlem7  9059  domunsn  9093  xpmapenlem  9110  infensuc  9121  findcard2d  9129  diffi  9137  cnvfi  9138  enreffi  9145  snnen2o  9183  1sdom2dom  9192  infi  9208  finresfin  9210  unblem1  9230  unblem2  9231  unblem3  9232  unblem4  9233  isfinite2  9236  infn0ALT  9241  unfilem1  9243  unfilem2  9244  unfir  9246  fofinf1o  9269  cnvfiALT  9276  mptfi  9288  finsschain  9296  imafi2  9298  marypha2  9379  inf0  9570  trcl  9677  frr3g  9708  r1rankidb  9756  snwf  9761  unwf  9762  uniwf  9771  rankval3b  9778  rankr1a  9788  rankxplim3  9833  scott0  9838  djueq1  9857  card1  9920  pm54.43  9953  infxpenc2  9972  dfac8clem  9982  alephsuc2  10030  alephle  10038  cardaleph  10039  dfac12lem2  10095  undjudom  10118  djudom1  10133  pwdju1  10141  nnadju  10148  ackbij1lem18  10186  cflem  10195  cflemOLD  10196  cflecard  10203  cfeq0  10207  cfslb  10217  cfsmolem  10221  cfcoflem  10223  cfidm  10226  isfin4p1  10266  fin23lem12  10282  fin23lem16  10286  fin23lem28  10291  fin23lem38  10300  fin23lem41  10303  fin1a2lem7  10357  fin1a2lem12  10362  fin1a2lem13  10363  hsmexlem8  10375  axcc2lem  10387  axcc3  10389  domtriomlem  10393  axdc3lem2  10402  axdc3lem4  10404  axdc4lem  10406  axcclem  10408  ac6num  10430  ttukeylem4  10463  ttukeylem7  10466  ttukey2g  10467  axdclem  10470  brdom3  10479  brdom5  10480  cardeq0  10503  unsnen  10504  konigthlem  10520  pwcfsdom  10535  canthp1lem1  10604  wunex2  10690  wuncval2  10699  eltsk2g  10703  ingru  10767  grutsk  10774  axgroth6  10780  mulidpi  10838  nlt1pi  10858  indpi  10859  pinq  10879  mulidnq  10915  1idpr  10981  prlem934  10985  0idsr  11049  1idsr  11050  00sr  11051  negexsr  11054  recexsrlem  11055  sqgt0sr  11058  ax1rid  11113  axcnre  11116  ne0gt0  11282  peano2cn  11349  peano2re  11350  00id  11352  mul02lem2  11354  mul01  11356  subid  11444  subid1  11445  negid  11472  negeq0  11479  peano2cnm  11491  peano2rem  11492  lt0neg1  11687  le0neg1  11689  relin01  11705  div2neg  11908  recgt0ii  12092  divgt0i2i  12101  ledivp1i  12111  ltdivp1i  12112  inelr  12179  indconst0  12201  indconst1  12202  peano5nni  12207  peano2nn  12216  nnge1  12235  nnne0  12241  times2  12348  addltmul  12451  nn0p1nn  12514  peano2nn0  12515  nn0lele2xi  12531  fcdmnn0supp  12532  fcdmnn0fsupp  12533  fcdmnn0suppg  12534  peano2z  12606  peano2zm  12608  suprzcl  12647  zeo  12653  eluzaddi  12864  uzwo  12906  uzwo2  12907  infssuzle  12926  infssuzcl  12927  zq  12949  rpnnen1lem1  12973  rpnnen1lem3  12974  rpnnen1lem5  12976  rphalfcl  13016  zgt1rpn0n1  13030  ltpnf  13116  nltmnf  13125  pnfge  13126  nltpnft  13161  xlemnf  13164  qsqueeze  13198  xlt0neg1  13216  xle0neg1  13218  xaddpnf1  13223  xaddmnf1  13225  xaddrid  13238  xsubge0  13258  xmul01  13264  xmulneg1  13266  xmulpnf1  13271  xmulrid  13276  supxrbnd  13325  supxrgtmnf  13326  supxrre1  13327  supxrre2  13328  elioopnf  13441  elicopnf  13443  iccshftri  13485  iccshftli  13487  iccdili  13489  icccntri  13491  fzprval  13584  fz0add1fz1  13735  fzofzp1  13764  fzostep1  13786  injresinj  13791  flge0nn0  13824  flge1nn  13825  btwnzge0  13832  modfrac  13888  om2uzsuci  13955  axdc4uzlem  13990  ser1const  14065  exp0  14072  exp1  14074  expn1  14078  nn0sqcl  14096  sqval  14121  sqeq0  14127  resqcl  14131  zsqcl  14136  expubnd  14185  binom21  14226  expnbnd  14239  nn0opthlem2  14276  bcnn  14319  bcn2  14326  bcn2p1  14332  bcnm1  14334  hasheq0  14370  hashsng  14376  hashen1  14377  hashunsnggt  14401  hashin  14418  hashdif  14420  hashgt23el  14431  hashxplem  14440  hashf1lem2  14463  hash2pr  14476  hash2prde  14477  pr2pwpr  14486  hash3tr  14498  iswrd  14522  wrdval  14523  hashwrdn  14554  ccatval2  14585  ccatrid  14595  eqs1  14620  s111  14623  ccatws1len  14628  repsw0  14784  repsw1  14790  cshw0  14801  wwlktovf  14963  relexpsucnnl  15037  reim0  15136  imval2  15169  cjne0  15181  abssq  15324  max0add  15328  abs2dif  15351  rddif  15359  absrdbnd  15360  rexuz3  15367  isershft  15682  isercolllem2  15684  isercoll  15686  fsum  15738  fsumadd  15758  fsumsplitsnun  15773  bcxmas  15856  infcvgaux2i  15879  fprod  15962  risefac0  16048  fallfac0  16049  risefac1  16054  fallfac1  16055  bpoly2  16078  bpoly3  16079  bpoly4  16080  fsumcube  16081  efi4p  16160  resin4p  16161  recos4p  16162  sinbnd  16203  cosbnd  16204  rpnnen2lem8  16244  rpnnen2lem12  16248  cnso  16270  dvdsmul2  16303  dvdslelem  16334  odd2np1lem  16365  mod2eq1n2dvds  16372  divalglem0  16418  divalglem1  16419  divalglem4  16421  divalglem5  16422  divalglem8  16425  flodddiv4  16440  bits0  16453  bitsp1o  16458  bitsf1  16471  sadadd2lem2  16475  gcd1  16553  lcm0val  16619  dvdslcm  16623  lcmeq0  16625  lcmgcd  16632  lcm1  16635  lcmfunsnlem2lem2  16664  lcmfunsnlem2  16665  prm2orodd  16716  phiprm  16803  pc0  16881  pcdvdstr  16903  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  hashbc0  17032  setsval  17194  fsets  17196  setsres  17205  ressinbas  17272  ressress  17274  elrestr  17448  pwssnf1o  17519  xpsfrnel  17583  xpscf  17586  ismred2  17622  submre  17624  mreacs  17681  oppchomfval  17737  brssc  17838  isssc  17844  yonedalem4c  18300  oduleval  18312  isprs  18319  oduclatb  18530  chninf  18658  gsumval2a  18710  smndex1n0mnd  18940  mulg1  19114  mulgnegnn  19117  ghmghmrn  19266  cntrnsg  19375  oppgplusfval  19379  pgrpsubgsymg  19440  psgneldm2i  19536  efgrelexlemb  19781  frgp0  19791  frgpmhm  19796  vrgpf  19799  cntrcmnd  19873  cntrabl  19874  cygctb  19923  dprd0  20064  dprd2da  20075  mgpplusg  20181  opprmulfval  20375  subrngint  20597  subrgint  20632  lsp0  21064  rlmval2  21247  cncrng  21433  cnfld1  21437  zringcyg  21509  mulgrhm2  21518  zlmsca  21560  fermltlchr  21569  chrnzr  21570  zrhpsgnelbas  21634  ocvz  21718  cssincl  21728  css0  21729  css1  21730  frlmip  21818  fczpsrbag  21961  ply1idvr1OLD  22346  evls1rhmlem  22372  evl1fval1lem  22381  marrepeval  22611  decpmatid  22818  0opn  22952  topopn  22954  basdif0  23001  tgval  23003  isopn2  23080  0cld  23086  ntropn  23097  ntrval2  23099  ntrdif  23100  clsdif  23101  cmclsopn  23110  ntrtop  23118  ntr0  23129  mretopd  23140  neips  23161  neiptopnei  23180  maxlp  23195  isperf2  23200  rest0  23217  iocpnfordt  23263  icomnfordt  23264  mnfnei  23269  refref  23561  unisngl  23575  1stckgen  23602  ptbasfi  23629  pthaus  23686  fbssfi  23885  isfil2  23904  ssfg  23920  filconn  23931  fbasrn  23932  filufint  23968  imaelfm  23999  fmfnfmlem4  24005  fclsfnflim  24075  alexsubALTlem3  24097  alexsubALTlem4  24098  ustfilxp  24261  ustuqtop2  24290  ustuqtop4  24292  utopsnneiplem  24295  utopsnnei  24297  utop2nei  24298  cfiluweak  24342  neipcfilu  24343  xmetres  24412  metres  24413  mopnex  24567  prdsms  24579  metucn  24619  tngds  24696  tngngp3  24704  nmoge0  24769  cnfldnm  24826  tgioo  24844  xrtgioo  24855  xrsmopn  24861  negcncf  24972  phtpy01  25035  pco0  25064  tcphtopn  25276  tchnmfval  25278  caussi  25347  rrxip  25440  minveclem3b  25478  ovolfioo  25517  ovolficc  25518  ovolfsf  25521  ovolctb  25540  ovolctb2  25542  ovolfiniun  25551  ovoliun2  25556  ovolshftlem1  25559  ovolscalem1  25563  ovolicopnf  25574  iunmbl2  25607  uniioombllem2  25633  opnmblALT  25653  ismbf  25678  mbfinf  25715  0plef  25722  itg1climres  25764  itg2cnlem1  25811  iblitg  25818  ibl0  25837  itgcn  25895  cnlimc  25938  dvfre  26001  dvnfre  26002  dveflem  26029  dvef  26030  dvlipcn  26044  lhop2  26065  itgsubstlem  26098  deg1val  26144  ply1rem  26214  coefv0  26296  plyrecj  26329  vieta1lem2  26363  aannenlem1  26380  aaliou2b  26393  ulmval  26431  ulmpm  26434  ulmdvlem1  26451  mtest  26455  efcn  26494  sin2pim  26538  cos2pim  26539  sinmpi  26540  cosmpi  26541  sinppi  26542  cosppi  26543  efimpi  26544  sincosq1lem  26550  sincosq2sgn  26552  sincosq3sgn  26553  sincosq4sgn  26554  sinq12gt0  26560  sinq34lt0t  26562  sincosq1eq  26565  abssinper  26574  efif1o  26599  loglt1b  26687  relogcn  26691  ellogdm  26692  efopn  26711  cxp0  26723  cxp1  26724  cxpsqrt  26756  logsqrt  26757  logb1  26822  atandm3  26931  atanbnd  26979  atancn  26989  leibpi  26995  efrlim  27022  logdifbnd  27046  vmaprm  27169  ppip1le  27213  ppieq0  27228  prmorcht  27230  ppiublem1  27254  ppiub  27256  chpeq0  27260  chtub  27264  fsumvma  27265  pclogsum  27267  chpval2  27270  dchrresb  27311  dchrptlem1  27316  lgs0  27362  lgs2  27366  lgsdir2lem2  27378  lgsdir2lem4  27380  lgsdchrval  27406  lgsdchr  27407  lgseisenlem2  27428  2lgslem1c  27445  2lgsoddprmlem2  27461  addsq2nreurex  27496  dirith2  27580  selberg2lem  27602  qabvle  27677  qabvexp  27678  ostth  27691  noextendseq  27719  noetasuplem4  27788  noetainflem4  27792  cutsun12  27871  madebdayim  27969  bdayiun  27996  addsrid  28045  addsfo  28064  peano2no  28065  negscl  28117  subsfo  28146  subsid1  28149  muls01  28193  mulsrid  28194  divs1  28285  recsex  28300  abssnid  28324  peano2ons  28361  noseqp1  28372  noseqind  28373  peano2nns  28431  n0fincut  28436  n0lts1e0  28449  dfnns2  28453  oldfib  28458  elzs2  28480  elnnzs  28482  elznns  28483  zsoring  28490  n0seo  28502  exps0  28508  exps1  28509  bdaypw2n0bndlem  28544  bdayfin  28568  istrkg2ld  28617  istrkg3ld  28618  ttgval  29032  brbtwn  29057  colinearalglem4  29067  upgr0eop  29272  uspgrushgr  29335  usgruspgr  29338  usgr0eop  29404  0grsubgr  29436  uspgrloopvtx  29673  umgr2v2evtx  29679  usgr0edg0rusgr  29733  rgrusgrprc  29747  wlkvtxiedg  29782  pthdivtx  29884  usgr2pthlem  29920  wlkswwlksf1o  30036  wwlksext2clwwlk  30216  konigsbergssiedgw  30409  frgrncvvdeqlem7  30464  2clwwlk2  30507  ex-po  30594  pliguhgr  30646  nvnd  30848  ipval2lem3  30865  ipval2  30867  ipidsq  30870  dipcj  30874  dip0r  30877  nmlnogt0  30957  blocni  30965  ipasslem2  30992  ipasslem8  30997  ipasslem9  30998  ajval  31021  ubthlem1  31030  hvaddlid  31183  hvsub0  31236  hi02  31257  hlimi  31348  isch2  31383  chlimi  31394  chsupunss  31504  shsupunss  31506  chlejb1i  31636  h1dei  31710  h1de2ci  31716  spanunsni  31739  pjoml2i  31745  pjorthi  31829  mayete3i  31888  hosubid1  31958  nmopge0  32071  nmfnge0  32087  adj1  32093  adjeq  32095  lnop0  32126  lnopmi  32160  nmophmi  32191  cnlnadjlem5  32231  cnlnadjeui  32237  unierri  32264  leoprf2  32287  leopnmid  32298  nmopleid  32299  hstles  32391  hst0  32393  strlem3a  32412  dmdbr2  32463  mdsl1i  32481  mdsl2i  32482  mdsl2bi  32483  cvmdi  32484  mdslmd1lem1  32485  mdslmd1lem2  32486  mdslmd1i  32489  mdslmd2i  32490  csmdsymi  32494  mdexchi  32495  superpos  32514  atomli  32542  atordi  32544  chirredlem1  32550  chirredlem2  32551  atcvat4i  32557  atabsi  32561  mdsymlem1  32563  mdsymlem5  32567  mdsymlem6  32568  sumdmdii  32575  dmdbr5ati  32582  dmdbr6ati  32583  mddmdin0i  32591  cdj3lem2  32595  unidifsnel  32694  unidifsnne  32695  xppreima  32808  abfmpunirn  32815  abfmpel  32818  aciunf1lem  32825  fgreu  32834  padct  32881  fpwrelmapffslem  32895  fpwrelmap  32896  xrge0infss  32923  xrdifh  32943  pfx1s2  33078  clatp0cl  33115  clatp1cl  33116  cntrcrng  33222  cycpmco2lem4  33270  rmfsupp2  33379  1fldgenq  33470  resvval  33476  rearchi  33493  qusxpid  33510  opprabs  33631  zringfrac  33711  psrbasfsupp  33769  0mplrim  33772  rlmdim  33868  constrfiss  34009  2sqr3minply  34038  locfinreflem  34098  locfinref  34099  ordtconnlem1  34182  rge0scvg  34207  lmxrge0  34210  qqh0  34242  qqh1  34243  rrh0  34273  zrhre  34277  esumcst  34321  esumfzf  34327  esumfsupre  34329  hasheuni  34343  sgon  34382  dmvlsiga  34387  sigainb  34394  measval  34456  ismeas  34457  sxbrsigalem0  34529  omssubadd  34558  carsggect  34576  eulerpartlemmf  34633  eulerpartlemgs2  34638  eulerpartlemn  34639  rrvsum  34712  ballotlem2  34747  ballotlemfcc  34752  ballotlem4  34757  signsplypnf  34805  signsply0  34806  signsw0glem  34808  signswrid  34813  signlem0  34842  signshf  34843  bnj535  35146  bnj580  35169  bnj907  35223  bnj1253  35273  funen1cnv  35343  rankval4b  35357  fineqvnttrclse  35381  noinfepfnregs  35389  onvf1odlem1  35407  onvf1od  35411  loop1cycl  35448  ptpconn  35544  cvmsss2  35585  cvmlift2lem12  35625  cvmlift2lem13  35626  cvmliftphtlem  35628  cvmliftpht  35629  fmlafvel  35696  mppsthm  35890  bcneg1  36047  fv1stcnv  36088  fv2ndcnv  36089  wlimeq1  36129  imagesset  36264  altopeq1  36274  brcolinear2  36369  nmulr0  36506  nmull0  36507  cldbnd  36647  ivthALT  36656  refssfne  36679  ontgval  36752  onint1  36770  ttcid  36813  ttcss  36819  ttcss2  36820  ttcsnexg  36841  ttcwf  36845  dfttc4lem2  36850  ttc0el  36856  axc11n11r  37119  bj-pm11.53a  37206  bj-bm1.3ii  37510  bj-restsn0  37536  bj-restsn10  37537  bj-restsnid  37538  bj-rest10  37539  bj-rest0  37544  bj-inftyexpiinv  37661  bj-inftyexpidisj  37663  taupilem1  37774  irrdiff  37779  qdiff  37780  f1omptsnlem  37791  mptsnunlem  37793  topdifinffinlem  37802  inunissunidif  37830  rdgssun  37833  exrecfnlem  37834  exrecfnpw  37836  finixpnum  38065  tan2h  38072  matunitlindflem2  38077  ptrest  38079  poimirlem22  38102  poimirlem25  38105  mblfinlem1  38117  mblfinlem2  38118  mblfinlem3  38119  mblfinlem4  38120  ismblfin  38121  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  itg2addnc  38134  itg2gt0cn  38135  ftc1anclem5  38157  ftc1anclem8  38160  dvasin  38164  dvacos  38165  sdclem2  38202  totbndbnd  38249  heibor1lem  38269  heiborlem7  38277  bfplem1  38282  prnc  38527  brxrn  38843  ecxrn2  38868  dfpeters2  39434  riotasv  39544  glbconN  39962  atpointN  40328  polsubN  40492  pol0N  40494  pol1N  40495  2polvalN  40499  2polssN  40500  3polN  40501  pcl0N  40507  2pmaplubN  40511  pnonsingN  40518  polsubclN  40537  cdlemefs32sn1aw  40999  cdleme43fsv1snlem  41005  cdleme41sn3a  41018  cdleme32a  41026  cdleme40m  41052  cdleme40n  41053  cdleme42b  41063  istendo  41345  cdlemk40  41502  cdlemkid  41521  dihvalcqpre  41820  facp2  42721  relt0neg1  43039  sn-nnne0  43043  frlmsnic  43119  prjspnerlem  43160  prjspnval2  43161  0prjspn  43171  3cubes  43232  mapfzcons1cl  43260  eldioph3b  43307  eldiophss  43316  0dioph  43320  vdioph  43321  eldioph4b  43349  eldioph4i  43350  rencldnfilem  43358  rmxy1  43460  rmxy0  43461  rmxm1  43472  rmym1  43473  monotoddzzfi  43480  wepwso  43581  aomclem6  43597  pwslnmlem0  43629  isnumbasabl  43644  areaquad  43754  onexlimgt  43781  oaabsb  43832  nadd1suc  43930  oe2  43943  safesnsupfidom1o  43954  onnoxp  43970  oa1cl  43984  finona1cl  43990  reabsifneg  44169  reabsifnneg  44172  relexp2  44214  eltrclrec  44217  elrtrclrec  44218  brtrclrec  44233  brrtrclrec  44234  relexpxpmin  44254  dftrcl3  44257  dfrtrcl3  44270  heeq1  44314  seff  44846  lhe4.4ex1a  44866  eelT0  45311  snssl  45366  sineq0ALT  45473  trfr  45499  xpwf  45501  dmwf  45502  rnwf  45503  modelaxreplem1  45515  modelaxreplem3  45517  0elaxnul  45520  prclaxpr  45522  uniclaxun  45523  wfac8prim  45539  permaxinf2lem  45549  elrnmpt1sf  45728  founiiun0  45729  supxrgere  45870  supxrgelem  45874  fmuldfeqlem1  46119  fmuldfeq  46120  climneg  46147  sumnnodd  46167  liminfltlem  46339  xlimpnfxnegmnf2  46393  addccncf2  46411  dvsinax  46448  stoweidlem18  46553  stoweidlem19  46554  stoweidlem22  46557  stoweidlem34  46569  stoweidlem40  46575  stoweidlem41  46576  stoweidlem55  46590  stoweidlem59  46594  dirker2re  46627  dirkerdenne0  46628  fourierdlem48  46689  fourierdlem49  46690  fourierdlem70  46711  fourierdlem71  46712  fourierdlem104  46745  fourierdlem112  46753  fouriersw  46766  etransclem46  46815  etransclem48  46817  nnfoctbdjlem  46990  ormklocald  47411  natlocalincr  47413  cjnpoly  47444  sinnpoly  47446  sqrtnegnre  47862  fsummmodsnunz  47938  flsqrt5  48164  bits0ALTV  48262  mogoldbblem  48303  sgoldbeven3prm  48366  nnsum3primes4  48371  isubgr0uhgr  48456  ushggricedg  48510  2zrngnmlid  48838  2zrngnmrid  48839  mpoexxg2  48921  lco0  49010  zlmodzxzldeplem3  49085  0dig1  49192  naryfvalel  49213  ackvalsuc0val  49270  iinxp  49413  0funclem  49668  aacllem  50383