Theorem mpan2 692

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr12  706  mp3an23  1456  elvd  3436  elabg  3620  eueq2  3657  sbcgf  3800  sbcralg  3813  csbconstgf  3856  sbcnestgw  4364  csbnestgw  4365  sbcnestg  4369  csbnestg  4370  csbnest1g  4373  iinexg  5285  eusv2nf  5332  reusv2lem5  5339  nnullss  5409  xpss1  5643  xpiindi  5784  reldm0  5877  elrnmpt1s  5908  resdm  5985  eliniseg  6053  trinxp  6082  ssrnres  6136  cnveq0  6155  coi2  6222  relrelss  6231  cnviin  6244  elpred  6276  onelssex  6366  ord0eln0  6373  funcnvres  6570  funimaex  6580  fnresin1  6617  fnresin2  6618  fresin  6703  ssimaex  6919  fvmpt  6941  fvmptnf  6964  fvimacnvALT  7003  dff3  7046  fsn  7082  fsn2  7083  funop  7096  fvrnressn  7108  fnsnbg  7112  fninfp  7122  fndifnfp  7124  fnnfpeq0  7126  fprb  7142  elabrex  7190  elabrexg  7191  f1elima  7211  f1ofvswap  7254  fliftel1  7258  f1owe  7301  sorpssuni  7679  sorpssint  7680  eldifpw  7715  ordeleqon  7729  ordsson  7730  ssnlim  7830  abrexexg  7907  tposfun  8185  tpostpos2  8190  fpr3g  8228  wfr3g  8262  tfrlem10  8319  tfrlem12  8321  tfr3  8331  seqomlem1  8382  seqomlem2  8383  seqomlem4  8385  ondif2  8430  oa0  8444  om0  8445  oa1suc  8459  om1  8470  oe1  8472  oe1m  8473  omass  8508  om2  8514  oeoalem  8525  oeoelem  8527  nnmsucr  8554  nnm1  8581  nnm2  8582  naddrid  8612  naddlid  8613  ecelqs  8707  xpider  8728  mapdm0  8782  fvdiagfn  8832  ixpsnf1o  8879  xp1en  8994  undom  8996  sbthlem7  9024  domunsn  9058  xpmapenlem  9075  infensuc  9086  findcard2d  9094  diffi  9102  cnvfi  9103  enreffi  9110  snnen2o  9148  1sdom2dom  9157  infi  9173  finresfin  9175  unblem1  9195  unblem2  9196  unblem3  9197  unblem4  9198  isfinite2  9201  infn0ALT  9206  unfilem1  9208  unfilem2  9209  unfir  9211  fofinf1o  9235  cnvfiALT  9242  mptfi  9254  finsschain  9262  imafi2  9264  marypha2  9345  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  20528  subrgint  20563  lsp0  20995  rlmval2  21179  cncrng  21378  cnfld1  21383  zringcyg  21459  mulgrhm2  21468  zlmsca  21510  fermltlchr  21519  chrnzr  21520  zrhpsgnelbas  21584  ocvz  21668  cssincl  21678  css0  21679  css1  21680  frlmip  21768  fczpsrbag  21911  ply1idvr1OLD  22270  evls1rhmlem  22296  evl1fval1lem  22305  marrepeval  22538  decpmatid  22745  0opn  22879  topopn  22881  basdif0  22928  tgval  22930  isopn2  23007  0cld  23013  ntropn  23024  ntrval2  23026  ntrdif  23027  clsdif  23028  cmclsopn  23037  ntrtop  23045  ntr0  23056  mretopd  23067  neips  23088  neiptopnei  23107  maxlp  23122  isperf2  23127  rest0  23144  iocpnfordt  23190  icomnfordt  23191  mnfnei  23196  refref  23488  unisngl  23502  1stckgen  23529  ptbasfi  23556  pthaus  23613  fbssfi  23812  isfil2  23831  ssfg  23847  filconn  23858  fbasrn  23859  filufint  23895  imaelfm  23926  fmfnfmlem4  23932  fclsfnflim  24002  alexsubALTlem3  24024  alexsubALTlem4  24025  ustfilxp  24188  ustuqtop2  24217  ustuqtop4  24219  utopsnneiplem  24222  utopsnnei  24224  utop2nei  24225  cfiluweak  24269  neipcfilu  24270  xmetres  24339  metres  24340  mopnex  24494  prdsms  24506  metucn  24546  tngds  24623  tngngp3  24631  nmoge0  24696  cnfldnm  24753  tgioo  24771  xrtgioo  24782  xrsmopn  24788  negcncf  24899  phtpy01  24962  pco0  24991  tcphtopn  25203  tchnmfval  25205  caussi  25274  rrxip  25367  minveclem3b  25405  ovolfioo  25444  ovolficc  25445  ovolfsf  25448  ovolctb  25467  ovolctb2  25469  ovolfiniun  25478  ovoliun2  25483  ovolshftlem1  25486  ovolscalem1  25490  ovolicopnf  25501  iunmbl2  25534  uniioombllem2  25560  opnmblALT  25580  ismbf  25605  mbfinf  25642  0plef  25649  itg1climres  25691  itg2cnlem1  25738  iblitg  25745  ibl0  25764  itgcn  25822  cnlimc  25865  dvfre  25928  dvnfre  25929  dveflem  25956  dvef  25957  dvlipcn  25971  lhop2  25992  itgsubstlem  26025  deg1val  26071  ply1rem  26141  coefv0  26223  plyrecj  26256  vieta1lem2  26288  aannenlem1  26305  aaliou2b  26318  ulmval  26358  ulmpm  26361  ulmdvlem1  26378  mtest  26382  efcn  26421  sin2pim  26462  cos2pim  26463  sinmpi  26464  cosmpi  26465  sinppi  26466  cosppi  26467  efimpi  26468  sincosq1lem  26474  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12gt0  26484  sinq34lt0t  26486  sincosq1eq  26489  abssinper  26498  efif1o  26523  loglt1b  26611  relogcn  26615  ellogdm  26616  efopn  26635  cxp0  26647  cxp1  26648  cxpsqrt  26680  logsqrt  26681  logb1  26746  atandm3  26855  atanbnd  26903  atancn  26913  leibpi  26919  efrlim  26946  efrlimOLD  26947  logdifbnd  26971  vmaprm  27094  ppip1le  27138  ppieq0  27153  prmorcht  27155  ppiublem1  27179  ppiub  27181  chpeq0  27185  chtub  27189  fsumvma  27190  pclogsum  27192  chpval2  27195  dchrresb  27236  dchrptlem1  27241  lgs0  27287  lgs2  27291  lgsdir2lem2  27303  lgsdir2lem4  27305  lgsdchrval  27331  lgsdchr  27332  lgseisenlem2  27353  2lgslem1c  27370  2lgsoddprmlem2  27386  addsq2nreurex  27421  dirith2  27505  selberg2lem  27527  qabvle  27602  qabvexp  27603  ostth  27616  noextendseq  27645  noetasuplem4  27714  noetainflem4  27718  cutsun12  27796  madebdayim  27894  bdayiun  27921  addsrid  27970  addsfo  27989  peano2no  27990  negscl  28042  subsfo  28071  subsid1  28074  muls01  28118  mulsrid  28119  divs1  28210  recsex  28225  abssnid  28249  peano2ons  28286  noseqp1  28297  noseqind  28298  peano2nns  28356  n0fincut  28361  n0lts1e0  28374  dfnns2  28378  oldfib  28383  elzs2  28405  elnnzs  28407  elznns  28408  zsoring  28415  n0seo  28427  exps0  28433  exps1  28434  bdaypw2n0bndlem  28469  bdayfin  28493  istrkg2ld  28542  istrkg3ld  28543  ttgval  28957  brbtwn  28982  colinearalglem4  28992  upgr0eop  29197  uspgrushgr  29260  usgruspgr  29263  usgr0eop  29329  0grsubgr  29361  uspgrloopvtx  29599  umgr2v2evtx  29605  usgr0edg0rusgr  29659  rgrusgrprc  29673  wlkvtxiedg  29708  pthdivtx  29810  usgr2pthlem  29846  wlkswwlksf1o  29962  wwlksext2clwwlk  30142  konigsbergssiedgw  30335  frgrncvvdeqlem7  30390  2clwwlk2  30433  ex-po  30520  pliguhgr  30572  nvnd  30774  ipval2lem3  30791  ipval2  30793  ipidsq  30796  dipcj  30800  dip0r  30803  nmlnogt0  30883  blocni  30891  ipasslem2  30918  ipasslem8  30923  ipasslem9  30924  ajval  30947  ubthlem1  30956  hvaddlid  31109  hvsub0  31162  hi02  31183  hlimi  31274  isch2  31309  chlimi  31320  chsupunss  31430  shsupunss  31432  chlejb1i  31562  h1dei  31636  h1de2ci  31642  spanunsni  31665  pjoml2i  31671  pjorthi  31755  mayete3i  31814  hosubid1  31884  nmopge0  31997  nmfnge0  32013  adj1  32019  adjeq  32021  lnop0  32052  lnopmi  32086  nmophmi  32117  cnlnadjlem5  32157  cnlnadjeui  32163  unierri  32190  leoprf2  32213  leopnmid  32224  nmopleid  32225  hstles  32317  hst0  32319  strlem3a  32338  dmdbr2  32389  mdsl1i  32407  mdsl2i  32408  mdsl2bi  32409  cvmdi  32410  mdslmd1lem1  32411  mdslmd1lem2  32412  mdslmd1i  32415  mdslmd2i  32416  csmdsymi  32420  mdexchi  32421  superpos  32440  atomli  32468  atordi  32470  chirredlem1  32476  chirredlem2  32477  atcvat4i  32483  atabsi  32487  mdsymlem1  32489  mdsymlem5  32493  mdsymlem6  32494  sumdmdii  32501  dmdbr5ati  32508  dmdbr6ati  32509  mddmdin0i  32517  cdj3lem2  32521  unidifsnel  32620  unidifsnne  32621  xppreima  32733  abfmpunirn  32740  abfmpel  32743  aciunf1lem  32750  fgreu  32759  padct  32806  fpwrelmapffslem  32820  fpwrelmap  32821  xrge0infss  32848  xrdifh  32868  pfx1s2  33014  clatp0cl  33051  clatp1cl  33052  cntrcrng  33157  cycpmco2lem4  33205  rmfsupp2  33314  1fldgenq  33398  resvval  33404  rearchi  33421  qusxpid  33438  opprabs  33557  zringfrac  33629  psrbasfsupp  33687  rlmdim  33769  constrfiss  33911  2sqr3minply  33940  locfinreflem  34000  locfinref  34001  ordtconnlem1  34084  rge0scvg  34109  lmxrge0  34112  qqh0  34144  qqh1  34145  rrh0  34175  zrhre  34179  esumcst  34223  esumfzf  34229  esumfsupre  34231  hasheuni  34245  sgon  34284  dmvlsiga  34289  sigainb  34296  measval  34358  ismeas  34359  sxbrsigalem0  34431  omssubadd  34460  carsggect  34478  eulerpartlemmf  34535  eulerpartlemgs2  34540  eulerpartlemn  34541  rrvsum  34614  ballotlem2  34649  ballotlemfcc  34654  ballotlem4  34659  signsplypnf  34710  signsply0  34711  signsw0glem  34713  signswrid  34718  signlem0  34747  signshf  34748  bnj535  35048  bnj580  35071  bnj907  35125  bnj1253  35175  funen1cnv  35247  rankval4b  35259  fineqvnttrclse  35284  noinfepfnregs  35292  onvf1odlem1  35301  onvf1od  35305  loop1cycl  35335  ptpconn  35431  cvmsss2  35472  cvmlift2lem12  35512  cvmlift2lem13  35513  cvmliftphtlem  35515  cvmliftpht  35516  fmlafvel  35583  mppsthm  35777  bcneg1  35934  fv1stcnv  35975  fv2ndcnv  35976  wlimeq1  36016  imagesset  36151  altopeq1  36161  brcolinear2  36256  cldbnd  36524  ivthALT  36533  refssfne  36556  ontgval  36629  onint1  36647  ttcid  36690  ttcss  36696  ttcss2  36697  ttcsnexg  36718  ttcwf  36722  dfttc4lem2  36727  ttc0el  36733  axc11n11r  36996  bj-pm11.53a  37083  bj-bm1.3ii  37387  bj-restsn0  37413  bj-restsn10  37414  bj-restsnid  37415  bj-rest10  37416  bj-rest0  37421  bj-inftyexpiinv  37538  bj-inftyexpidisj  37540  taupilem1  37651  irrdiff  37656  f1omptsnlem  37666  mptsnunlem  37668  topdifinffinlem  37677  inunissunidif  37705  rdgssun  37708  exrecfnlem  37709  exrecfnpw  37711  finixpnum  37940  tan2h  37947  matunitlindflem2  37952  ptrest  37954  poimirlem22  37977  poimirlem25  37980  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  ftc1anclem5  38032  ftc1anclem8  38035  dvasin  38039  dvacos  38040  sdclem2  38077  totbndbnd  38124  heibor1lem  38144  heiborlem7  38152  bfplem1  38157  prnc  38402  brxrn  38718  ecxrn2  38743  dfpeters2  39309  riotasv  39419  glbconN  39837  atpointN  40203  polsubN  40367  pol0N  40369  pol1N  40370  2polvalN  40374  2polssN  40375  3polN  40376  pcl0N  40382  2pmaplubN  40386  pnonsingN  40393  polsubclN  40412  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdleme41sn3a  40893  cdleme32a  40901  cdleme40m  40927  cdleme40n  40928  cdleme42b  40938  istendo  41220  cdlemk40  41377  cdlemkid  41396  dihvalcqpre  41695  facp2  42596  relt0neg1  42915  sn-nnne0  42919  frlmsnic  42999  prjspnerlem  43064  prjspnval2  43065  0prjspn  43075  3cubes  43136  mapfzcons1cl  43164  eldioph3b  43211  eldiophss  43220  0dioph  43224  vdioph  43225  eldioph4b  43257  eldioph4i  43258  rencldnfilem  43266  rmxy1  43368  rmxy0  43369  rmxm1  43380  rmym1  43381  monotoddzzfi  43388  wepwso  43489  aomclem6  43505  pwslnmlem0  43537  isnumbasabl  43552  areaquad  43662  onexlimgt  43689  oaabsb  43740  nadd1suc  43838  oe2  43851  safesnsupfidom1o  43862  onnoxp  43878  oa1cl  43892  finona1cl  43898  reabsifneg  44077  reabsifnneg  44080  relexp2  44122  eltrclrec  44125  elrtrclrec  44126  brtrclrec  44141  brrtrclrec  44142  relexpxpmin  44162  dftrcl3  44165  dfrtrcl3  44178  heeq1  44222  seff  44754  lhe4.4ex1a  44774  eelT0  45219  snssl  45274  sineq0ALT  45381  trfr  45407  xpwf  45409  dmwf  45410  rnwf  45411  modelaxreplem1  45423  modelaxreplem3  45425  0elaxnul  45428  prclaxpr  45430  uniclaxun  45431  wfac8prim  45447  permaxinf2lem  45457  elrnmpt1sf  45637  founiiun0  45638  supxrgere  45781  supxrgelem  45785  fmuldfeqlem1  46030  fmuldfeq  46031  climneg  46058  sumnnodd  46078  liminfltlem  46250  xlimpnfxnegmnf2  46304  addccncf2  46322  dvsinax  46359  stoweidlem18  46464  stoweidlem19  46465  stoweidlem22  46468  stoweidlem34  46480  stoweidlem40  46486  stoweidlem41  46487  stoweidlem55  46501  stoweidlem59  46505  dirker2re  46538  dirkerdenne0  46539  fourierdlem48  46600  fourierdlem49  46601  fourierdlem70  46622  fourierdlem71  46623  fourierdlem104  46656  fourierdlem112  46664  fouriersw  46677  etransclem46  46726  etransclem48  46728  nnfoctbdjlem  46901  ormklocald  47320  natlocalincr  47322  cjnpoly  47349  sinnpoly  47351  sqrtnegnre  47767  fsummmodsnunz  47843  flsqrt5  48069  bits0ALTV  48167  mogoldbblem  48208  sgoldbeven3prm  48271  nnsum3primes4  48276  isubgr0uhgr  48361  ushggricedg  48415  2zrngnmlid  48743  2zrngnmrid  48744  mpoexxg2  48826  lco0  48915  zlmodzxzldeplem3  48990  0dig1  49097  naryfvalel  49118  ackvalsuc0val  49175  iinxp  49318  0funclem  49573  aacllem  50288