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  3435  elabg  3619  eueq2  3656  sbcgf  3799  sbcralg  3812  csbconstgf  3855  sbcnestgw  4363  csbnestgw  4364  sbcnestg  4368  csbnestg  4369  csbnest1g  4372  iinexg  5289  eusv2nf  5337  reusv2lem5  5344  nnullss  5414  xpss1  5650  xpiindi  5790  reldm0  5883  elrnmpt1s  5914  resdm  5991  eliniseg  6059  trinxp  6088  ssrnres  6142  cnveq0  6161  coi2  6228  relrelss  6237  cnviin  6250  elpred  6282  onelssex  6372  ord0eln0  6379  funcnvres  6576  funimaex  6586  fnresin1  6623  fnresin2  6624  fresin  6709  ssimaex  6925  fvmpt  6947  fvmptnf  6970  fvimacnvALT  7009  dff3  7052  fsn  7088  fsn2  7089  funop  7103  fvrnressn  7115  fnsnbg  7119  fninfp  7129  fndifnfp  7131  fnnfpeq0  7133  fprb  7149  elabrex  7197  elabrexg  7198  f1elima  7218  f1ofvswap  7261  fliftel1  7265  f1owe  7308  sorpssuni  7686  sorpssint  7687  eldifpw  7722  ordeleqon  7736  ordsson  7737  ssnlim  7837  abrexexg  7914  tposfun  8192  tpostpos2  8197  fpr3g  8235  wfr3g  8269  tfrlem10  8326  tfrlem12  8328  tfr3  8338  seqomlem1  8389  seqomlem2  8390  seqomlem4  8392  ondif2  8437  oa0  8451  om0  8452  oa1suc  8466  om1  8477  oe1  8479  oe1m  8480  omass  8515  om2  8521  oeoalem  8532  oeoelem  8534  nnmsucr  8561  nnm1  8588  nnm2  8589  naddrid  8619  naddlid  8620  ecelqs  8714  xpider  8735  mapdm0  8789  fvdiagfn  8839  ixpsnf1o  8886  xp1en  9001  undom  9003  sbthlem7  9031  domunsn  9065  xpmapenlem  9082  infensuc  9093  findcard2d  9101  diffi  9109  cnvfi  9110  enreffi  9117  snnen2o  9155  1sdom2dom  9164  infi  9180  finresfin  9182  unblem1  9202  unblem2  9203  unblem3  9204  unblem4  9205  isfinite2  9208  infn0ALT  9213  unfilem1  9215  unfilem2  9216  unfir  9218  fofinf1o  9242  cnvfiALT  9249  mptfi  9261  finsschain  9269  imafi2  9271  marypha2  9352  inf0  9542  trcl  9649  frr3g  9680  r1rankidb  9728  snwf  9733  unwf  9734  uniwf  9743  rankval3b  9750  rankr1a  9760  rankxplim3  9805  scott0  9810  djueq1  9829  card1  9892  pm54.43  9925  infxpenc2  9944  dfac8clem  9954  alephsuc2  10002  alephle  10010  cardaleph  10011  dfac12lem2  10067  undjudom  10090  djudom1  10105  pwdju1  10113  nnadju  10120  ackbij1lem18  10158  cflem  10167  cflemOLD  10168  cflecard  10175  cfeq0  10178  cfslb  10188  cfsmolem  10192  cfcoflem  10194  cfidm  10197  isfin4p1  10237  fin23lem12  10253  fin23lem16  10257  fin23lem28  10262  fin23lem38  10271  fin23lem41  10274  fin1a2lem7  10328  fin1a2lem12  10333  fin1a2lem13  10334  hsmexlem8  10346  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ac6num  10401  ttukeylem4  10434  ttukeylem7  10437  ttukey2g  10438  axdclem  10441  brdom3  10450  brdom5  10451  cardeq0  10474  unsnen  10475  konigthlem  10491  pwcfsdom  10506  canthp1lem1  10575  wunex2  10661  wuncval2  10670  eltsk2g  10674  ingru  10738  grutsk  10745  axgroth6  10751  mulidpi  10809  nlt1pi  10829  indpi  10830  pinq  10850  mulidnq  10886  1idpr  10952  prlem934  10956  0idsr  11020  1idsr  11021  00sr  11022  negexsr  11025  recexsrlem  11026  sqgt0sr  11029  ax1rid  11084  axcnre  11087  ne0gt0  11251  peano2cn  11318  peano2re  11319  00id  11321  mul02lem2  11323  mul01  11325  subid  11413  subid1  11414  negid  11441  negeq0  11448  peano2cnm  11460  peano2rem  11461  lt0neg1  11656  le0neg1  11658  relin01  11674  div2neg  11878  recgt0ii  12062  divgt0i2i  12071  ledivp1i  12081  ltdivp1i  12082  inelr  12149  indconst0  12171  indconst1  12172  peano5nni  12177  peano2nn  12186  nnge1  12205  nnne0  12211  times2  12313  addltmul  12413  nn0p1nn  12476  peano2nn0  12477  nn0lele2xi  12493  fcdmnn0supp  12494  fcdmnn0fsupp  12495  fcdmnn0suppg  12496  peano2z  12568  peano2zm  12570  suprzcl  12609  zeo  12615  eluzaddi  12819  uzwo  12861  uzwo2  12862  infssuzle  12881  infssuzcl  12882  zq  12904  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  rphalfcl  12971  zgt1rpn0n1  12985  ltpnf  13071  nltmnf  13080  pnfge  13081  nltpnft  13116  xlemnf  13119  qsqueeze  13153  xlt0neg1  13171  xle0neg1  13173  xaddpnf1  13178  xaddmnf1  13180  xaddrid  13193  xsubge0  13213  xmul01  13219  xmulneg1  13221  xmulpnf1  13226  xmulrid  13231  supxrbnd  13280  supxrgtmnf  13281  supxrre1  13282  supxrre2  13283  elioopnf  13396  elicopnf  13398  iccshftri  13440  iccshftli  13442  iccdili  13444  icccntri  13446  fzprval  13539  fz0add1fz1  13690  fzofzp1  13719  fzostep1  13741  injresinj  13746  flge0nn0  13779  flge1nn  13780  btwnzge0  13787  modfrac  13843  om2uzsuci  13910  axdc4uzlem  13945  ser1const  14020  exp0  14027  exp1  14029  expn1  14033  nn0sqcl  14051  sqval  14076  sqeq0  14082  resqcl  14086  zsqcl  14091  expubnd  14140  binom21  14181  expnbnd  14194  nn0opthlem2  14231  bcnn  14274  bcn2  14281  bcn2p1  14287  bcnm1  14289  hasheq0  14325  hashsng  14331  hashen1  14332  hashunsnggt  14356  hashin  14373  hashdif  14375  hashgt23el  14386  hashxplem  14395  hashf1lem2  14418  hash2pr  14431  hash2prde  14432  pr2pwpr  14441  hash3tr  14453  iswrd  14477  wrdval  14478  hashwrdn  14509  ccatval2  14540  ccatrid  14550  eqs1  14575  s111  14578  ccatws1len  14583  repsw0  14739  repsw1  14745  cshw0  14756  wwlktovf  14918  relexpsucnnl  14992  reim0  15080  imval2  15113  cjne0  15125  abssq  15268  max0add  15272  abs2dif  15295  rddif  15303  absrdbnd  15304  rexuz3  15311  isershft  15626  isercolllem2  15628  isercoll  15630  fsum  15682  fsumadd  15702  fsumsplitsnun  15717  bcxmas  15800  infcvgaux2i  15823  fprod  15906  risefac0  15992  fallfac0  15993  risefac1  15998  fallfac1  15999  bpoly2  16022  bpoly3  16023  bpoly4  16024  fsumcube  16025  efi4p  16104  resin4p  16105  recos4p  16106  sinbnd  16147  cosbnd  16148  rpnnen2lem8  16188  rpnnen2lem12  16192  cnso  16214  dvdsmul2  16247  dvdslelem  16278  odd2np1lem  16309  mod2eq1n2dvds  16316  divalglem0  16362  divalglem1  16363  divalglem4  16365  divalglem5  16366  divalglem8  16369  flodddiv4  16384  bits0  16397  bitsp1o  16402  bitsf1  16415  sadadd2lem2  16419  gcd1  16497  lcm0val  16563  dvdslcm  16567  lcmeq0  16569  lcmgcd  16576  lcm1  16579  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  prm2orodd  16660  phiprm  16747  pc0  16825  pcdvdstr  16847  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  hashbc0  16976  setsval  17137  fsets  17139  setsres  17148  ressinbas  17215  ressress  17217  elrestr  17391  pwssnf1o  17462  xpsfrnel  17526  xpscf  17529  ismred2  17565  submre  17567  mreacs  17624  oppchomfval  17680  brssc  17781  isssc  17787  yonedalem4c  18243  oduleval  18255  isprs  18262  oduclatb  18473  chninf  18601  gsumval2a  18653  smndex1n0mnd  18883  mulg1  19057  mulgnegnn  19060  isghmOLD  19191  ghmghmrn  19210  cntrnsg  19319  oppgplusfval  19323  pgrpsubgsymg  19384  psgneldm2i  19480  efgrelexlemb  19725  frgp0  19735  frgpmhm  19740  vrgpf  19743  cntrcmnd  19817  cntrabl  19818  cygctb  19867  dprd0  20008  dprd2da  20019  mgpplusg  20125  opprmulfval  20319  subrngint  20537  subrgint  20572  lsp0  21004  rlmval2  21187  cncrng  21373  cnfld1  21377  zringcyg  21449  mulgrhm2  21458  zlmsca  21500  fermltlchr  21509  chrnzr  21510  zrhpsgnelbas  21574  ocvz  21658  cssincl  21668  css0  21669  css1  21670  frlmip  21758  fczpsrbag  21901  ply1idvr1OLD  22260  evls1rhmlem  22286  evl1fval1lem  22295  marrepeval  22528  decpmatid  22735  0opn  22869  topopn  22871  basdif0  22918  tgval  22920  isopn2  22997  0cld  23003  ntropn  23014  ntrval2  23016  ntrdif  23017  clsdif  23018  cmclsopn  23027  ntrtop  23035  ntr0  23046  mretopd  23057  neips  23078  neiptopnei  23097  maxlp  23112  isperf2  23117  rest0  23134  iocpnfordt  23180  icomnfordt  23181  mnfnei  23186  refref  23478  unisngl  23492  1stckgen  23519  ptbasfi  23546  pthaus  23603  fbssfi  23802  isfil2  23821  ssfg  23837  filconn  23848  fbasrn  23849  filufint  23885  imaelfm  23916  fmfnfmlem4  23922  fclsfnflim  23992  alexsubALTlem3  24014  alexsubALTlem4  24015  ustfilxp  24178  ustuqtop2  24207  ustuqtop4  24209  utopsnneiplem  24212  utopsnnei  24214  utop2nei  24215  cfiluweak  24259  neipcfilu  24260  xmetres  24329  metres  24330  mopnex  24484  prdsms  24496  metucn  24536  tngds  24613  tngngp3  24621  nmoge0  24686  cnfldnm  24743  tgioo  24761  xrtgioo  24772  xrsmopn  24778  negcncf  24889  phtpy01  24952  pco0  24981  tcphtopn  25193  tchnmfval  25195  caussi  25264  rrxip  25357  minveclem3b  25395  ovolfioo  25434  ovolficc  25435  ovolfsf  25438  ovolctb  25457  ovolctb2  25459  ovolfiniun  25468  ovoliun2  25473  ovolshftlem1  25476  ovolscalem1  25480  ovolicopnf  25491  iunmbl2  25524  uniioombllem2  25550  opnmblALT  25570  ismbf  25595  mbfinf  25632  0plef  25639  itg1climres  25681  itg2cnlem1  25728  iblitg  25735  ibl0  25754  itgcn  25812  cnlimc  25855  dvfre  25918  dvnfre  25919  dveflem  25946  dvef  25947  dvlipcn  25961  lhop2  25982  itgsubstlem  26015  deg1val  26061  ply1rem  26131  coefv0  26213  plyrecj  26246  vieta1lem2  26277  aannenlem1  26294  aaliou2b  26307  ulmval  26345  ulmpm  26348  ulmdvlem1  26365  mtest  26369  efcn  26408  sin2pim  26449  cos2pim  26450  sinmpi  26451  cosmpi  26452  sinppi  26453  cosppi  26454  efimpi  26455  sincosq1lem  26461  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  sinq12gt0  26471  sinq34lt0t  26473  sincosq1eq  26476  abssinper  26485  efif1o  26510  loglt1b  26598  relogcn  26602  ellogdm  26603  efopn  26622  cxp0  26634  cxp1  26635  cxpsqrt  26667  logsqrt  26668  logb1  26733  atandm3  26842  atanbnd  26890  atancn  26900  leibpi  26906  efrlim  26933  logdifbnd  26957  vmaprm  27080  ppip1le  27124  ppieq0  27139  prmorcht  27141  ppiublem1  27165  ppiub  27167  chpeq0  27171  chtub  27175  fsumvma  27176  pclogsum  27178  chpval2  27181  dchrresb  27222  dchrptlem1  27227  lgs0  27273  lgs2  27277  lgsdir2lem2  27289  lgsdir2lem4  27291  lgsdchrval  27317  lgsdchr  27318  lgseisenlem2  27339  2lgslem1c  27356  2lgsoddprmlem2  27372  addsq2nreurex  27407  dirith2  27491  selberg2lem  27513  qabvle  27588  qabvexp  27589  ostth  27602  noextendseq  27631  noetasuplem4  27700  noetainflem4  27704  cutsun12  27782  madebdayim  27880  bdayiun  27907  addsrid  27956  addsfo  27975  peano2no  27976  negscl  28028  subsfo  28057  subsid1  28060  muls01  28104  mulsrid  28105  divs1  28196  recsex  28211  abssnid  28235  peano2ons  28272  noseqp1  28283  noseqind  28284  peano2nns  28342  n0fincut  28347  n0lts1e0  28360  dfnns2  28364  oldfib  28369  elzs2  28391  elnnzs  28393  elznns  28394  zsoring  28401  n0seo  28413  exps0  28419  exps1  28420  bdaypw2n0bndlem  28455  bdayfin  28479  istrkg2ld  28528  istrkg3ld  28529  ttgval  28943  brbtwn  28968  colinearalglem4  28978  upgr0eop  29183  uspgrushgr  29246  usgruspgr  29249  usgr0eop  29315  0grsubgr  29347  uspgrloopvtx  29584  umgr2v2evtx  29590  usgr0edg0rusgr  29644  rgrusgrprc  29658  wlkvtxiedg  29693  pthdivtx  29795  usgr2pthlem  29831  wlkswwlksf1o  29947  wwlksext2clwwlk  30127  konigsbergssiedgw  30320  frgrncvvdeqlem7  30375  2clwwlk2  30418  ex-po  30505  pliguhgr  30557  nvnd  30759  ipval2lem3  30776  ipval2  30778  ipidsq  30781  dipcj  30785  dip0r  30788  nmlnogt0  30868  blocni  30876  ipasslem2  30903  ipasslem8  30908  ipasslem9  30909  ajval  30932  ubthlem1  30941  hvaddlid  31094  hvsub0  31147  hi02  31168  hlimi  31259  isch2  31294  chlimi  31305  chsupunss  31415  shsupunss  31417  chlejb1i  31547  h1dei  31621  h1de2ci  31627  spanunsni  31650  pjoml2i  31656  pjorthi  31740  mayete3i  31799  hosubid1  31869  nmopge0  31982  nmfnge0  31998  adj1  32004  adjeq  32006  lnop0  32037  lnopmi  32071  nmophmi  32102  cnlnadjlem5  32142  cnlnadjeui  32148  unierri  32175  leoprf2  32198  leopnmid  32209  nmopleid  32210  hstles  32302  hst0  32304  strlem3a  32323  dmdbr2  32374  mdsl1i  32392  mdsl2i  32393  mdsl2bi  32394  cvmdi  32395  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd1i  32400  mdslmd2i  32401  csmdsymi  32405  mdexchi  32406  superpos  32425  atomli  32453  atordi  32455  chirredlem1  32461  chirredlem2  32462  atcvat4i  32468  atabsi  32472  mdsymlem1  32474  mdsymlem5  32478  mdsymlem6  32479  sumdmdii  32486  dmdbr5ati  32493  dmdbr6ati  32494  mddmdin0i  32502  cdj3lem2  32506  unidifsnel  32605  unidifsnne  32606  xppreima  32718  abfmpunirn  32725  abfmpel  32728  aciunf1lem  32735  fgreu  32744  padct  32791  fpwrelmapffslem  32805  fpwrelmap  32806  xrge0infss  32833  xrdifh  32853  pfx1s2  32999  clatp0cl  33036  clatp1cl  33037  cntrcrng  33142  cycpmco2lem4  33190  rmfsupp2  33299  1fldgenq  33383  resvval  33389  rearchi  33406  qusxpid  33423  opprabs  33542  zringfrac  33614  psrbasfsupp  33672  rlmdim  33754  constrfiss  33895  2sqr3minply  33924  locfinreflem  33984  locfinref  33985  ordtconnlem1  34068  rge0scvg  34093  lmxrge0  34096  qqh0  34128  qqh1  34129  rrh0  34159  zrhre  34163  esumcst  34207  esumfzf  34213  esumfsupre  34215  hasheuni  34229  sgon  34268  dmvlsiga  34273  sigainb  34280  measval  34342  ismeas  34343  sxbrsigalem0  34415  omssubadd  34444  carsggect  34462  eulerpartlemmf  34519  eulerpartlemgs2  34524  eulerpartlemn  34525  rrvsum  34598  ballotlem2  34633  ballotlemfcc  34638  ballotlem4  34643  signsplypnf  34694  signsply0  34695  signsw0glem  34697  signswrid  34702  signlem0  34731  signshf  34732  bnj535  35032  bnj580  35055  bnj907  35109  bnj1253  35159  funen1cnv  35231  rankval4b  35243  fineqvnttrclse  35268  noinfepfnregs  35276  onvf1odlem1  35285  onvf1od  35289  loop1cycl  35319  ptpconn  35415  cvmsss2  35456  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmliftphtlem  35499  cvmliftpht  35500  fmlafvel  35567  mppsthm  35761  bcneg1  35918  fv1stcnv  35959  fv2ndcnv  35960  wlimeq1  36000  imagesset  36135  altopeq1  36145  brcolinear2  36240  cldbnd  36508  ivthALT  36517  refssfne  36540  ontgval  36613  onint1  36631  ttcid  36674  ttcss  36680  ttcss2  36681  ttcsnexg  36702  ttcwf  36706  dfttc4lem2  36711  ttc0el  36717  axc11n11r  36980  bj-pm11.53a  37067  bj-bm1.3ii  37371  bj-restsn0  37397  bj-restsn10  37398  bj-restsnid  37399  bj-rest10  37400  bj-rest0  37405  bj-inftyexpiinv  37522  bj-inftyexpidisj  37524  taupilem1  37635  irrdiff  37640  qdiff  37641  f1omptsnlem  37652  mptsnunlem  37654  topdifinffinlem  37663  inunissunidif  37691  rdgssun  37694  exrecfnlem  37695  exrecfnpw  37697  finixpnum  37926  tan2h  37933  matunitlindflem2  37938  ptrest  37940  poimirlem22  37963  poimirlem25  37966  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ftc1anclem5  38018  ftc1anclem8  38021  dvasin  38025  dvacos  38026  sdclem2  38063  totbndbnd  38110  heibor1lem  38130  heiborlem7  38138  bfplem1  38143  prnc  38388  brxrn  38704  ecxrn2  38729  dfpeters2  39295  riotasv  39405  glbconN  39823  atpointN  40189  polsubN  40353  pol0N  40355  pol1N  40356  2polvalN  40360  2polssN  40361  3polN  40362  pcl0N  40368  2pmaplubN  40372  pnonsingN  40379  polsubclN  40398  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32a  40887  cdleme40m  40913  cdleme40n  40914  cdleme42b  40924  istendo  41206  cdlemk40  41363  cdlemkid  41382  dihvalcqpre  41681  facp2  42582  relt0neg1  42901  sn-nnne0  42905  frlmsnic  42985  prjspnerlem  43050  prjspnval2  43051  0prjspn  43061  3cubes  43122  mapfzcons1cl  43150  eldioph3b  43197  eldiophss  43206  0dioph  43210  vdioph  43211  eldioph4b  43239  eldioph4i  43240  rencldnfilem  43248  rmxy1  43350  rmxy0  43351  rmxm1  43362  rmym1  43363  monotoddzzfi  43370  wepwso  43471  aomclem6  43487  pwslnmlem0  43519  isnumbasabl  43534  areaquad  43644  onexlimgt  43671  oaabsb  43722  nadd1suc  43820  oe2  43833  safesnsupfidom1o  43844  onnoxp  43860  oa1cl  43874  finona1cl  43880  reabsifneg  44059  reabsifnneg  44062  relexp2  44104  eltrclrec  44107  elrtrclrec  44108  brtrclrec  44123  brrtrclrec  44124  relexpxpmin  44144  dftrcl3  44147  dfrtrcl3  44160  heeq1  44204  seff  44736  lhe4.4ex1a  44756  eelT0  45201  snssl  45256  sineq0ALT  45363  trfr  45389  xpwf  45391  dmwf  45392  rnwf  45393  modelaxreplem1  45405  modelaxreplem3  45407  0elaxnul  45410  prclaxpr  45412  uniclaxun  45413  wfac8prim  45429  permaxinf2lem  45439  elrnmpt1sf  45619  founiiun0  45620  supxrgere  45763  supxrgelem  45767  fmuldfeqlem1  46012  fmuldfeq  46013  climneg  46040  sumnnodd  46060  liminfltlem  46232  xlimpnfxnegmnf2  46286  addccncf2  46304  dvsinax  46341  stoweidlem18  46446  stoweidlem19  46447  stoweidlem22  46450  stoweidlem34  46462  stoweidlem40  46468  stoweidlem41  46469  stoweidlem55  46483  stoweidlem59  46487  dirker2re  46520  dirkerdenne0  46521  fourierdlem48  46582  fourierdlem49  46583  fourierdlem70  46604  fourierdlem71  46605  fourierdlem104  46638  fourierdlem112  46646  fouriersw  46659  etransclem46  46708  etransclem48  46710  nnfoctbdjlem  46883  ormklocald  47304  natlocalincr  47306  cjnpoly  47337  sinnpoly  47339  sqrtnegnre  47755  fsummmodsnunz  47831  flsqrt5  48057  bits0ALTV  48155  mogoldbblem  48196  sgoldbeven3prm  48259  nnsum3primes4  48264  isubgr0uhgr  48349  ushggricedg  48403  2zrngnmlid  48731  2zrngnmrid  48732  mpoexxg2  48814  lco0  48903  zlmodzxzldeplem3  48978  0dig1  49085  naryfvalel  49106  ackvalsuc0val  49163  iinxp  49306  0funclem  49561  aacllem  50276