Theorem mpan2 703

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanr12  717  mp3an23  1479  elvd  3469  elabg  3644  eueq2  3682  sbcgf  3823  sbcralg  3836  csbconstgf  3879  sbcnestgw  4386  csbnestgw  4387  sbcnestg  4391  csbnestg  4392  csbnest1g  4395  iinexg  5316  eusv2nf  5364  reusv2lem5  5371  nnullss  5441  xpss1  5678  xpiindi  5819  reldm0  5916  elrnmpt1s  5947  resdm  6023  eliniseg  6094  trinxp  6123  ssrnres  6174  cnveq0  6194  coi2  6263  relrelss  6272  cnviin  6285  elpred  6317  onelssex  6408  ord0eln0  6415  funcnvres  6612  funimaex  6621  fnresin1  6658  fnresin2  6659  fresin  6745  ssimaex  6964  fvmpt  6987  fvmptnf  7010  fvimacnvALT  7050  dff3  7093  fsn  7129  fsn2  7130  funop  7144  fvrnressn  7156  fnsnbg  7160  fninfp  7170  fndifnfp  7172  fnnfpeq0  7174  fprb  7190  elabrex  7238  elabrexg  7239  f1elima  7259  f1ofvswap  7302  fliftel1  7306  f1owe  7349  sorpssuni  7727  sorpssint  7728  eldifpw  7763  ordeleqon  7777  ordsson  7778  ssnlim  7878  abrexexg  7954  tposfun  8234  tpostpos2  8239  fpr3g  8278  wfr3g  8312  tfrlem10  8370  tfrlem12  8372  tfr3  8382  seqomlem1  8433  seqomlem2  8434  seqomlem4  8436  ondif2  8483  oa0  8497  om0  8498  oa1suc  8512  om1  8523  oe1  8525  oe1m  8526  omass  8561  om2  8567  oeoalem  8578  oeoelem  8580  nnmsucr  8607  nnm1  8634  nnm2  8635  naddrid  8666  naddlid  8667  ecelqs  8761  xpider  8782  mapdm0  8835  fvdiagfn  8885  ixpsnf1o  8932  xp1en  9047  undom  9049  sbthlem7  9077  domunsn  9111  xpmapenlem  9128  infensuc  9139  findcard2d  9147  diffi  9155  cnvfi  9156  enreffi  9163  snnen2o  9201  1sdom2dom  9210  infi  9226  finresfin  9228  unblem1  9248  unblem2  9249  unblem3  9250  unblem4  9251  isfinite2  9254  infn0ALT  9259  unfilem1  9261  unfilem2  9262  unfir  9264  fofinf1o  9285  cnvfiALT  9292  mptfi  9304  finsschain  9312  imafi2  9314  marypha2  9395  inf0  9586  trcl  9693  frr3g  9724  r1rankidb  9772  snwf  9777  unwf  9778  uniwf  9787  rankval3b  9794  rankr1a  9804  rankxplim3  9849  scott0  9856  djueq1  9887  card1  9950  pm54.43  9983  infxpenc2  10002  dfac8clem  10012  alephsuc2  10060  alephle  10068  cardaleph  10069  dfac12lem2  10124  undjudom  10147  djudom1  10162  pwdju1  10170  nnadju  10177  ackbij1lem18  10215  cflem  10224  cflemOLD  10225  cflecard  10232  cfeq0  10236  cfslb  10246  cfsmolem  10250  cfcoflem  10252  cfidm  10255  isfin4p1  10295  fin23lem12  10311  fin23lem16  10315  fin23lem28  10320  fin23lem38  10329  fin23lem41  10332  fin1a2lem7  10386  fin1a2lem12  10391  fin1a2lem13  10392  hsmexlem8  10404  axcc2lem  10416  axcc3  10418  domtriomlem  10422  axdc3lem2  10431  axdc3lem4  10433  axdc4lem  10435  axcclem  10437  ac6num  10459  ttukeylem4  10492  ttukeylem7  10495  ttukey2g  10496  axdclem  10499  brdom3  10508  brdom5  10509  cardeq0  10532  unsnen  10533  konigthlem  10549  pwcfsdom  10564  canthp1lem1  10633  wunex2  10719  wuncval2  10728  eltsk2g  10732  ingru  10796  grutsk  10803  axgroth6  10809  mulidpi  10867  nlt1pi  10887  indpi  10888  pinq  10908  mulidnq  10944  1idpr  11010  prlem934  11014  0idsr  11078  1idsr  11079  00sr  11080  negexsr  11083  recexsrlem  11084  sqgt0sr  11087  ax1rid  11142  axcnre  11145  ne0gt0  11311  peano2cn  11378  peano2re  11379  00id  11381  mul02lem2  11383  mul01  11385  subid  11473  subid1  11474  negid  11501  negeq0  11508  peano2cnm  11520  peano2rem  11521  lt0neg1  11716  le0neg1  11718  relin01  11734  div2neg  11934  recgt0ii  12117  divgt0i2i  12126  ledivp1i  12136  ltdivp1i  12137  inelr  12204  indconst0  12226  indconst1  12227  peano5nni  12232  peano2nn  12241  nnge1  12260  nnne0  12266  times2  12373  addltmul  12476  nn0p1nn  12539  peano2nn0  12540  nn0lele2xi  12556  fcdmnn0supp  12557  fcdmnn0fsupp  12558  fcdmnn0suppg  12559  peano2z  12631  peano2zm  12633  suprzcl  12672  zeo  12678  eluzaddi  12889  uzwo  12931  uzwo2  12932  infssuzle  12951  infssuzcl  12952  zq  12974  rpnnen1lem1  12998  rpnnen1lem3  12999  rpnnen1lem5  13001  rphalfcl  13041  zgt1rpn0n1  13055  ltpnf  13141  nltmnf  13150  pnfge  13151  nltpnft  13186  xlemnf  13189  qsqueeze  13223  xlt0neg1  13241  xle0neg1  13243  xaddpnf1  13248  xaddmnf1  13250  xaddrid  13263  xsubge0  13283  xmul01  13289  xmulneg1  13291  xmulpnf1  13296  xmulrid  13301  supxrbnd  13350  supxrgtmnf  13351  supxrre1  13352  supxrre2  13353  elioopnf  13466  elicopnf  13468  iccshftri  13510  iccshftli  13512  iccdili  13514  icccntri  13516  fzprval  13609  fz0add1fz1  13760  fzofzp1  13789  fzostep1  13811  injresinj  13816  flge0nn0  13849  flge1nn  13850  btwnzge0  13857  modfrac  13913  om2uzsuci  13980  axdc4uzlem  14015  ser1const  14090  exp0  14097  exp1  14099  expn1  14103  nn0sqcl  14121  sqval  14146  sqeq0  14152  resqcl  14156  zsqcl  14161  expubnd  14210  binom21  14251  expnbnd  14264  nn0opthlem2  14301  bcnn  14344  bcn2  14351  bcn2p1  14357  bcnm1  14359  hasheq0  14395  hashsng  14401  hashen1  14402  hashunsnggt  14426  hashin  14444  hashdif  14446  hashgt23el  14457  hashxplem  14466  hashf1lem2  14489  hash2pr  14502  hash2prde  14503  pr2pwpr  14512  hash3tr  14524  iswrd  14548  wrdval  14549  hashwrdn  14580  ccatval2  14611  ccatrid  14621  eqs1  14646  s111  14649  ccatws1len  14654  repsw0  14810  repsw1  14816  cshw0  14827  wwlktovf  14989  relexpsucnnl  15063  reim0  15165  imval2  15198  cjne0  15210  abssq  15353  max0add  15357  abs2dif  15380  rddif  15388  absrdbnd  15389  rexuz3  15396  isershft  15711  isercolllem2  15713  isercoll  15715  fsum  15767  fsumadd  15787  fsumsplitsnun  15802  bcxmas  15885  infcvgaux2i  15908  fprod  15991  risefac0  16077  fallfac0  16078  risefac1  16083  fallfac1  16084  bpoly2  16107  bpoly3  16108  bpoly4  16109  fsumcube  16110  efi4p  16189  resin4p  16190  recos4p  16191  sinbnd  16232  cosbnd  16233  rpnnen2lem8  16273  rpnnen2lem12  16277  cnso  16299  dvdsmul2  16332  dvdslelem  16363  odd2np1lem  16394  mod2eq1n2dvds  16401  divalglem0  16447  divalglem1  16448  divalglem4  16450  divalglem5  16451  divalglem8  16454  flodddiv4  16469  bits0  16482  bitsp1o  16487  bitsf1  16500  sadadd2lem2  16504  gcd1  16582  lcm0val  16648  dvdslcm  16652  lcmeq0  16654  lcmgcd  16661  lcm1  16664  lcmfunsnlem2lem2  16693  lcmfunsnlem2  16694  prm2orodd  16745  phiprm  16832  pc0  16910  pcdvdstr  16932  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  hashbc0  17061  setsval  17223  fsets  17225  setsres  17234  ressinbas  17301  ressress  17303  elrestr  17477  pwssnf1o  17548  xpsfrnel  17612  xpscf  17615  ismred2  17651  submre  17653  mreacs  17710  oppchomfval  17766  brssc  17867  isssc  17873  yonedalem4c  18329  oduleval  18341  isprs  18348  oduclatb  18559  chninf  18687  gsumval2a  18739  smndex1n0mnd  18970  mulg1  19143  mulgnegnn  19146  qusxpid  19247  ghmghmrn  19301  cntrnsg  19410  oppgplusfval  19414  pgrpsubgsymg  19475  psgneldm2i  19571  efgrelexlemb  19816  frgp0  19826  frgpmhm  19831  vrgpf  19834  cntrcmnd  19908  cntrabl  19909  cygctb  19958  dprd0  20099  dprd2da  20110  mgpplusg  20216  opprmulfval  20417  subrngint  20641  subrgint  20676  lsp0  21104  rlmval2  21287  cncrng  21508  cnfld1  21512  zringcyg  21584  mulgrhm2  21593  zlmsca  21635  fermltlchr  21644  chrnzr  21645  zrhpsgnelbas  21709  ocvz  21793  cssincl  21803  css0  21804  css1  21805  frlmip  21893  fczpsrbag  22036  evls1rhmlem  22446  evl1fval1lem  22455  marrepeval  22685  decpmatid  22892  0opn  23026  topopn  23028  basdif0  23075  tgval  23077  isopn2  23154  0cld  23160  ntropn  23171  ntrval2  23173  ntrdif  23174  clsdif  23175  cmclsopn  23184  ntrtop  23192  ntr0  23203  mretopd  23214  neips  23235  neiptopnei  23254  maxlp  23269  isperf2  23274  rest0  23291  iocpnfordt  23337  icomnfordt  23338  mnfnei  23343  refref  23635  unisngl  23649  1stckgen  23676  ptbasfi  23703  pthaus  23760  fbssfi  23959  isfil2  23978  ssfg  23994  filconn  24005  fbasrn  24006  filufint  24042  imaelfm  24073  fmfnfmlem4  24079  fclsfnflim  24149  alexsubALTlem3  24171  alexsubALTlem4  24172  ustfilxp  24335  ustuqtop2  24364  ustuqtop4  24366  utopsnneiplem  24369  utopsnnei  24371  utop2nei  24372  cfiluweak  24416  neipcfilu  24417  xmetres  24486  metres  24487  mopnex  24641  prdsms  24653  metucn  24693  tngds  24770  tngngp3  24778  nmoge0  24843  cnfldnm  24900  tgioo  24918  xrtgioo  24929  xrsmopn  24935  negcncf  25046  phtpy01  25109  pco0  25138  tcphtopn  25350  tchnmfval  25352  caussi  25421  rrxip  25514  minveclem3b  25552  ovolfioo  25591  ovolficc  25592  ovolfsf  25595  ovolctb  25614  ovolctb2  25616  ovolfiniun  25625  ovoliun2  25630  ovolshftlem1  25633  ovolscalem1  25637  ovolicopnf  25648  iunmbl2  25681  uniioombllem2  25707  opnmblALT  25727  ismbf  25752  mbfinf  25789  0plef  25796  itg1climres  25838  itg2cnlem1  25885  iblitg  25892  ibl0  25911  itgcn  25969  cnlimc  26012  dvfre  26075  dvnfre  26076  dveflem  26103  dvef  26104  dvlipcn  26118  lhop2  26139  itgsubstlem  26172  deg1val  26218  ply1rem  26288  coefv0  26370  plyrecj  26403  vieta1lem2  26437  aannenlem1  26454  aaliou2b  26467  ulmval  26505  ulmpm  26508  ulmdvlem1  26525  mtest  26529  efcn  26568  sin2pim  26612  cos2pim  26613  sinmpi  26614  cosmpi  26615  sinppi  26616  cosppi  26617  efimpi  26618  sincosq1lem  26624  sincosq2sgn  26626  sincosq3sgn  26627  sincosq4sgn  26628  sinq12gt0  26634  sinq34lt0t  26636  sincosq1eq  26639  abssinper  26648  efif1o  26673  loglt1b  26761  relogcn  26765  ellogdm  26766  efopn  26785  cxp0  26797  cxp1  26798  cxpsqrt  26830  logsqrt  26831  logb1  26896  atandm3  27005  atanbnd  27053  atancn  27063  leibpi  27069  efrlim  27096  logdifbnd  27120  vmaprm  27243  ppip1le  27287  ppieq0  27302  prmorcht  27304  ppiublem1  27328  ppiub  27330  chpeq0  27334  chtub  27338  fsumvma  27339  pclogsum  27341  chpval2  27344  dchrresb  27385  dchrptlem1  27390  lgs0  27436  lgs2  27440  lgsdir2lem2  27452  lgsdir2lem4  27454  lgsdchrval  27480  lgsdchr  27481  lgseisenlem2  27502  2lgslem1c  27519  2lgsoddprmlem2  27535  addsq2nreurex  27570  dirith2  27654  selberg2lem  27676  qabvle  27751  qabvexp  27752  ostth  27765  noextendseq  27793  noetasuplem4  27862  noetainflem4  27866  cutsun12  27945  madebdayim  28043  bdayiun  28070  addsrid  28119  addsfo  28138  peano2no  28139  negscl  28191  subsfo  28220  subsid1  28223  muls01  28267  mulsrid  28268  divs1  28359  recsex  28374  abssnid  28398  peano2ons  28435  noseqp1  28446  noseqind  28447  peano2nns  28505  n0fincut  28510  n0lts1e0  28523  dfnns2  28527  oldfib  28532  elzs2  28554  elnnzs  28556  elznns  28557  zsoring  28564  n0seo  28576  exps0  28582  exps1  28583  bdaypw2n0bndlem  28618  bdayfin  28642  istrkg2ld  28691  istrkg3ld  28692  ttgval  29161  brbtwn  29186  colinearalglem4  29196  upgr0eop  29401  uspgrushgr  29464  usgruspgr  29467  usgr0eop  29533  0grsubgr  29565  uspgrloopvtx  29802  umgr2v2evtx  29808  usgr0edg0rusgr  29862  rgrusgrprc  29876  wlkvtxiedg  29911  pthdivtx  30013  usgr2pthlem  30049  wlkswwlksf1o  30165  wwlksext2clwwlk  30345  konigsbergssiedgw  30538  frgrncvvdeqlem7  30593  2clwwlk2  30636  ex-po  30723  pliguhgr  30775  nvnd  30977  ipval2lem3  30994  ipval2  30996  ipidsq  30999  dipcj  31003  dip0r  31006  nmlnogt0  31086  blocni  31094  ipasslem2  31121  ipasslem8  31126  ipasslem9  31127  ajval  31150  ubthlem1  31159  hvaddlid  31312  hvsub0  31365  hi02  31386  hlimi  31477  isch2  31512  chlimi  31523  chsupunss  31633  shsupunss  31635  chlejb1i  31765  h1dei  31839  h1de2ci  31845  spanunsni  31868  pjoml2i  31874  pjorthi  31958  mayete3i  32017  hosubid1  32087  nmopge0  32200  nmfnge0  32216  adj1  32222  adjeq  32224  lnop0  32255  lnopmi  32289  nmophmi  32320  cnlnadjlem5  32360  cnlnadjeui  32366  unierri  32393  leoprf2  32416  leopnmid  32427  nmopleid  32428  hstles  32520  hst0  32522  strlem3a  32541  dmdbr2  32592  mdsl1i  32610  mdsl2i  32611  mdsl2bi  32612  cvmdi  32613  mdslmd1lem1  32614  mdslmd1lem2  32615  mdslmd1i  32618  mdslmd2i  32619  csmdsymi  32623  mdexchi  32624  superpos  32643  atomli  32671  atordi  32673  chirredlem1  32679  chirredlem2  32680  atcvat4i  32686  atabsi  32690  mdsymlem1  32692  mdsymlem5  32696  mdsymlem6  32697  sumdmdii  32704  dmdbr5ati  32711  dmdbr6ati  32712  mddmdin0i  32720  cdj3lem2  32724  unidifsnel  32818  unidifsnne  32819  xppreima  32927  abfmpunirn  32934  abfmpel  32937  aciunf1lem  32944  fgreu  32953  padct  33000  fpwrelmapffslem  33014  fpwrelmap  33015  xrge0infss  33042  xrdifh  33062  pfx1s2  33196  clatp0cl  33233  clatp1cl  33234  cntrcrng  33338  cycpmco2lem4  33386  rmfsupp2  33494  1fldgenq  33582  resvval  33588  rearchi  33605  opprabs  33705  zringfrac  33785  psrbasfsupp  33842  0mplrim  33845  rlmdim  33941  constrfiss  34082  2sqr3minply  34111  locfinreflem  34171  locfinref  34172  ordtconnlem1  34255  rge0scvg  34280  lmxrge0  34283  qqh0  34315  qqh1  34316  rrh0  34346  zrhre  34350  esumcst  34394  esumfzf  34400  esumfsupre  34402  hasheuni  34416  sgon  34455  dmvlsiga  34460  sigainb  34467  measval  34529  ismeas  34530  sxbrsigalem0  34602  omssubadd  34631  carsggect  34649  eulerpartlemmf  34706  eulerpartlemgs2  34711  eulerpartlemn  34712  rrvsum  34785  ballotlem2  34820  ballotlemfcc  34825  ballotlem4  34830  signsplypnf  34878  signsply0  34879  signsw0glem  34881  signswrid  34886  signlem0  34915  signshf  34916  bnj535  35219  bnj580  35242  bnj907  35296  bnj1253  35346  funen1cnv  35416  rankval4b  35432  fineqvnttrclse  35456  noinfepfnregs  35464  onvf1odlem1  35482  onvf1od  35486  loop1cycl  35524  ptpconn  35620  cvmsss2  35661  cvmlift2lem12  35701  cvmlift2lem13  35702  cvmliftphtlem  35704  cvmliftpht  35705  fmlafvel  35772  mppsthm  35966  bcneg1  36123  fv1stcnv  36164  fv2ndcnv  36165  wlimeq1  36205  imagesset  36340  altopeq1  36350  brcolinear2  36445  nmulr0  36582  nmull0  36583  cldbnd  36722  ivthALT  36731  refssfne  36754  ontgval  36827  onint1  36845  ttcid  36888  ttcss  36894  ttcss2  36895  ttcsnexg  36916  ttcwf  36920  dfttc4lem2  36925  ttc0el  36931  axc11n11r  37193  bj-pm11.53a  37280  bj-bm1.3ii  37584  bj-restsn0  37610  bj-restsn10  37611  bj-restsnid  37612  bj-rest10  37613  bj-rest0  37618  bj-inftyexpiinv  37735  bj-inftyexpidisj  37737  taupilem1  37848  irrdiff  37853  qdiff  37854  f1omptsnlem  37865  mptsnunlem  37867  topdifinffinlem  37876  inunissunidif  37904  rdgssun  37907  exrecfnlem  37908  exrecfnpw  37910  finixpnum  38139  tan2h  38146  matunitlindflem2  38151  ptrest  38153  poimirlem22  38176  poimirlem25  38179  mblfinlem1  38191  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  itg2addnclem  38205  itg2addnclem2  38206  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  ftc1anclem5  38231  ftc1anclem8  38234  dvasin  38238  dvacos  38239  sdclem2  38276  totbndbnd  38323  heibor1lem  38343  heiborlem7  38351  bfplem1  38356  prnc  38601  brxrn  38917  ecxrn2  38942  dfpeters2  39508  riotasv  39618  glbconN  40036  atpointN  40402  polsubN  40566  pol0N  40568  pol1N  40569  2polvalN  40573  2polssN  40574  3polN  40575  pcl0N  40581  2pmaplubN  40585  pnonsingN  40592  polsubclN  40611  cdlemefs32sn1aw  41073  cdleme43fsv1snlem  41079  cdleme41sn3a  41092  cdleme32a  41100  cdleme40m  41126  cdleme40n  41127  cdleme42b  41137  istendo  41419  cdlemk40  41576  cdlemkid  41595  dihvalcqpre  41894  facp2  42795  relt0neg1  43115  sn-nnne0  43119  frlmsnic  43195  prjspnerlem  43236  prjspnval2  43237  0prjspn  43247  3cubes  43308  mapfzcons1cl  43336  eldioph3b  43383  eldiophss  43392  0dioph  43396  vdioph  43397  eldioph4b  43425  eldioph4i  43426  rencldnfilem  43434  rmxy1  43536  rmxy0  43537  rmxm1  43548  rmym1  43549  monotoddzzfi  43556  wepwso  43657  aomclem6  43673  pwslnmlem0  43705  isnumbasabl  43720  areaquad  43830  onexlimgt  43857  oaabsb  43908  nadd1suc  44006  oe2  44019  safesnsupfidom1o  44030  onnoxp  44046  oa1cl  44060  finona1cl  44066  reabsifneg  44245  reabsifnneg  44248  relexp2  44290  eltrclrec  44293  elrtrclrec  44294  brtrclrec  44309  brrtrclrec  44310  relexpxpmin  44330  dftrcl3  44333  dfrtrcl3  44346  heeq1  44390  seff  44906  lhe4.4ex1a  44926  eelT0  45370  snssl  45425  sineq0ALT  45532  trfr  45558  xpwf  45560  dmwf  45561  rnwf  45562  modelaxreplem1  45574  modelaxreplem3  45576  0elaxnul  45579  prclaxpr  45581  uniclaxun  45582  wfac8prim  45598  permaxinf2lem  45608  hashnnsuc  45616  elrnmpt1sf  45794  founiiun0  45795  supxrgere  45936  supxrgelem  45940  fmuldfeqlem1  46185  fmuldfeq  46186  climneg  46213  sumnnodd  46233  liminfltlem  46405  xlimpnfxnegmnf2  46459  addccncf2  46477  dvsinax  46514  stoweidlem18  46619  stoweidlem19  46620  stoweidlem22  46623  stoweidlem34  46635  stoweidlem40  46641  stoweidlem41  46642  stoweidlem55  46656  stoweidlem59  46660  dirker2re  46693  dirkerdenne0  46694  fourierdlem48  46755  fourierdlem49  46756  fourierdlem70  46777  fourierdlem71  46778  fourierdlem104  46811  fourierdlem112  46819  fouriersw  46832  etransclem46  46881  etransclem48  46883  nnfoctbdjlem  47056  ormklocald  47477  natlocalincr  47479  cjnpoly  47510  sinnpoly  47512  sqrtnegnre  47928  fsummmodsnunz  48004  flsqrt5  48230  bits0ALTV  48328  mogoldbblem  48369  sgoldbeven3prm  48432  nnsum3primes4  48437  isubgr0uhgr  48522  ushggricedg  48576  2zrngnmlid  48904  2zrngnmrid  48905  mpoexxg2  48998  lco0  49087  zlmodzxzldeplem3  49162  0dig1  49269  naryfvalel  49290  ackvalsuc0val  49347  iinxp  49489  0funclem  49744  aacllem  50470