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  5283  eusv2nf  5330  reusv2lem5  5337  nnullss  5407  xpss1  5641  xpiindi  5782  reldm0  5875  elrnmpt1s  5906  resdm  5983  eliniseg  6051  trinxp  6080  ssrnres  6134  cnveq0  6153  coi2  6220  relrelss  6229  cnviin  6242  elpred  6274  onelssex  6364  ord0eln0  6371  funcnvres  6568  funimaex  6578  fnresin1  6615  fnresin2  6616  fresin  6701  ssimaex  6917  fvmpt  6939  fvmptnf  6962  fvimacnvALT  7001  dff3  7044  fsn  7080  fsn2  7081  funop  7094  fvrnressn  7106  fnsnbg  7110  fninfp  7120  fndifnfp  7122  fnnfpeq0  7124  fprb  7140  elabrex  7188  elabrexg  7189  f1elima  7209  f1ofvswap  7252  fliftel1  7256  f1owe  7299  sorpssuni  7677  sorpssint  7678  eldifpw  7713  ordeleqon  7727  ordsson  7728  ssnlim  7828  abrexexg  7905  tposfun  8183  tpostpos2  8188  fpr3g  8226  wfr3g  8260  tfrlem10  8317  tfrlem12  8319  tfr3  8329  seqomlem1  8380  seqomlem2  8381  seqomlem4  8383  ondif2  8428  oa0  8442  om0  8443  oa1suc  8457  om1  8468  oe1  8470  oe1m  8471  omass  8506  om2  8512  oeoalem  8523  oeoelem  8525  nnmsucr  8552  nnm1  8579  nnm2  8580  naddrid  8610  naddlid  8611  ecelqs  8705  xpider  8726  mapdm0  8780  fvdiagfn  8830  ixpsnf1o  8877  xp1en  8992  undom  8994  sbthlem7  9022  domunsn  9056  xpmapenlem  9073  infensuc  9084  findcard2d  9092  diffi  9100  cnvfi  9101  enreffi  9108  snnen2o  9146  1sdom2dom  9155  infi  9171  finresfin  9173  unblem1  9193  unblem2  9194  unblem3  9195  unblem4  9196  isfinite2  9199  infn0ALT  9204  unfilem1  9206  unfilem2  9207  unfir  9209  fofinf1o  9233  cnvfiALT  9240  mptfi  9252  finsschain  9260  imafi2  9262  marypha2  9343  inf0  9531  trcl  9638  frr3g  9669  r1rankidb  9717  snwf  9722  unwf  9723  uniwf  9732  rankval3b  9739  rankr1a  9749  rankxplim3  9794  scott0  9799  djueq1  9818  card1  9881  pm54.43  9914  infxpenc2  9933  dfac8clem  9943  alephsuc2  9991  alephle  9999  cardaleph  10000  dfac12lem2  10056  undjudom  10079  djudom1  10094  pwdju1  10102  nnadju  10109  ackbij1lem18  10147  cflem  10156  cflemOLD  10157  cflecard  10164  cfeq0  10167  cfslb  10177  cfsmolem  10181  cfcoflem  10183  cfidm  10186  isfin4p1  10226  fin23lem12  10242  fin23lem16  10246  fin23lem28  10251  fin23lem38  10260  fin23lem41  10263  fin1a2lem7  10317  fin1a2lem12  10322  fin1a2lem13  10323  hsmexlem8  10335  axcc2lem  10347  axcc3  10349  domtriomlem  10353  axdc3lem2  10362  axdc3lem4  10364  axdc4lem  10366  axcclem  10368  ac6num  10390  ttukeylem4  10423  ttukeylem7  10426  ttukey2g  10427  axdclem  10430  brdom3  10439  brdom5  10440  cardeq0  10463  unsnen  10464  konigthlem  10480  pwcfsdom  10495  canthp1lem1  10564  wunex2  10650  wuncval2  10659  eltsk2g  10663  ingru  10727  grutsk  10734  axgroth6  10740  mulidpi  10798  nlt1pi  10818  indpi  10819  pinq  10839  mulidnq  10875  1idpr  10941  prlem934  10945  0idsr  11009  1idsr  11010  00sr  11011  negexsr  11014  recexsrlem  11015  sqgt0sr  11018  ax1rid  11073  axcnre  11076  ne0gt0  11240  peano2cn  11307  peano2re  11308  00id  11310  mul02lem2  11312  mul01  11314  subid  11402  subid1  11403  negid  11430  negeq0  11437  peano2cnm  11449  peano2rem  11450  lt0neg1  11645  le0neg1  11647  relin01  11663  div2neg  11867  recgt0ii  12051  divgt0i2i  12060  ledivp1i  12070  ltdivp1i  12071  inelr  12138  indconst0  12160  indconst1  12161  peano5nni  12166  peano2nn  12175  nnge1  12194  nnne0  12200  times2  12302  addltmul  12402  nn0p1nn  12465  peano2nn0  12466  nn0lele2xi  12482  fcdmnn0supp  12483  fcdmnn0fsupp  12484  fcdmnn0suppg  12485  peano2z  12557  peano2zm  12559  suprzcl  12598  zeo  12604  eluzaddi  12808  uzwo  12850  uzwo2  12851  infssuzle  12870  infssuzcl  12871  zq  12893  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem5  12920  rphalfcl  12960  zgt1rpn0n1  12974  ltpnf  13060  nltmnf  13069  pnfge  13070  nltpnft  13105  xlemnf  13108  qsqueeze  13142  xlt0neg1  13160  xle0neg1  13162  xaddpnf1  13167  xaddmnf1  13169  xaddrid  13182  xsubge0  13202  xmul01  13208  xmulneg1  13210  xmulpnf1  13215  xmulrid  13220  supxrbnd  13269  supxrgtmnf  13270  supxrre1  13271  supxrre2  13272  elioopnf  13385  elicopnf  13387  iccshftri  13429  iccshftli  13431  iccdili  13433  icccntri  13435  fzprval  13528  fz0add1fz1  13679  fzofzp1  13708  fzostep1  13730  injresinj  13735  flge0nn0  13768  flge1nn  13769  btwnzge0  13776  modfrac  13832  om2uzsuci  13899  axdc4uzlem  13934  ser1const  14009  exp0  14016  exp1  14018  expn1  14022  nn0sqcl  14040  sqval  14065  sqeq0  14071  resqcl  14075  zsqcl  14080  expubnd  14129  binom21  14170  expnbnd  14183  nn0opthlem2  14220  bcnn  14263  bcn2  14270  bcn2p1  14276  bcnm1  14278  hasheq0  14314  hashsng  14320  hashen1  14321  hashunsnggt  14345  hashin  14362  hashdif  14364  hashgt23el  14375  hashxplem  14384  hashf1lem2  14407  hash2pr  14420  hash2prde  14421  pr2pwpr  14430  hash3tr  14442  iswrd  14466  wrdval  14467  hashwrdn  14498  ccatval2  14529  ccatrid  14539  eqs1  14564  s111  14567  ccatws1len  14572  repsw0  14728  repsw1  14734  cshw0  14745  wwlktovf  14907  relexpsucnnl  14981  reim0  15069  imval2  15102  cjne0  15114  abssq  15257  max0add  15261  abs2dif  15284  rddif  15292  absrdbnd  15293  rexuz3  15300  isershft  15615  isercolllem2  15617  isercoll  15619  fsum  15671  fsumadd  15691  fsumsplitsnun  15706  bcxmas  15789  infcvgaux2i  15812  fprod  15895  risefac0  15981  fallfac0  15982  risefac1  15987  fallfac1  15988  bpoly2  16011  bpoly3  16012  bpoly4  16013  fsumcube  16014  efi4p  16093  resin4p  16094  recos4p  16095  sinbnd  16136  cosbnd  16137  rpnnen2lem8  16177  rpnnen2lem12  16181  cnso  16203  dvdsmul2  16236  dvdslelem  16267  odd2np1lem  16298  mod2eq1n2dvds  16305  divalglem0  16351  divalglem1  16352  divalglem4  16354  divalglem5  16355  divalglem8  16358  flodddiv4  16373  bits0  16386  bitsp1o  16391  bitsf1  16404  sadadd2lem2  16408  gcd1  16486  lcm0val  16552  dvdslcm  16556  lcmeq0  16558  lcmgcd  16565  lcm1  16568  lcmfunsnlem2lem2  16597  lcmfunsnlem2  16598  prm2orodd  16649  phiprm  16736  pc0  16814  pcdvdstr  16836  vdwlem2  16942  vdwlem6  16946  vdwlem8  16948  hashbc0  16965  setsval  17126  fsets  17128  setsres  17137  ressinbas  17204  ressress  17206  elrestr  17380  pwssnf1o  17451  xpsfrnel  17515  xpscf  17518  ismred2  17554  submre  17556  mreacs  17613  oppchomfval  17669  brssc  17770  isssc  17776  yonedalem4c  18232  oduleval  18244  isprs  18251  oduclatb  18462  chninf  18590  gsumval2a  18642  smndex1n0mnd  18872  mulg1  19046  mulgnegnn  19049  isghmOLD  19180  ghmghmrn  19199  cntrnsg  19308  oppgplusfval  19312  pgrpsubgsymg  19373  psgneldm2i  19469  efgrelexlemb  19714  frgp0  19724  frgpmhm  19729  vrgpf  19732  cntrcmnd  19806  cntrabl  19807  cygctb  19856  dprd0  19997  dprd2da  20008  mgpplusg  20114  opprmulfval  20308  subrngint  20526  subrgint  20561  lsp0  20993  rlmval2  21177  cncrng  21376  cnfld1  21381  zringcyg  21457  mulgrhm2  21466  zlmsca  21508  fermltlchr  21517  chrnzr  21518  zrhpsgnelbas  21582  ocvz  21666  cssincl  21676  css0  21677  css1  21678  frlmip  21766  fczpsrbag  21909  ply1idvr1OLD  22269  evls1rhmlem  22295  evl1fval1lem  22304  marrepeval  22537  decpmatid  22744  0opn  22878  topopn  22880  basdif0  22927  tgval  22929  isopn2  23006  0cld  23012  ntropn  23023  ntrval2  23025  ntrdif  23026  clsdif  23027  cmclsopn  23036  ntrtop  23044  ntr0  23055  mretopd  23066  neips  23087  neiptopnei  23106  maxlp  23121  isperf2  23126  rest0  23143  iocpnfordt  23189  icomnfordt  23190  mnfnei  23195  refref  23487  unisngl  23501  1stckgen  23528  ptbasfi  23555  pthaus  23612  fbssfi  23811  isfil2  23830  ssfg  23846  filconn  23857  fbasrn  23858  filufint  23894  imaelfm  23925  fmfnfmlem4  23931  fclsfnflim  24001  alexsubALTlem3  24023  alexsubALTlem4  24024  ustfilxp  24187  ustuqtop2  24216  ustuqtop4  24218  utopsnneiplem  24221  utopsnnei  24223  utop2nei  24224  cfiluweak  24268  neipcfilu  24269  xmetres  24338  metres  24339  mopnex  24493  prdsms  24505  metucn  24545  tngds  24622  tngngp3  24630  nmoge0  24695  cnfldnm  24752  tgioo  24770  xrtgioo  24781  xrsmopn  24787  negcncf  24898  phtpy01  24961  pco0  24990  tcphtopn  25202  tchnmfval  25204  caussi  25273  rrxip  25366  minveclem3b  25404  ovolfioo  25443  ovolficc  25444  ovolfsf  25447  ovolctb  25466  ovolctb2  25468  ovolfiniun  25477  ovoliun2  25482  ovolshftlem1  25485  ovolscalem1  25489  ovolicopnf  25500  iunmbl2  25533  uniioombllem2  25559  opnmblALT  25579  ismbf  25604  mbfinf  25641  0plef  25648  itg1climres  25690  itg2cnlem1  25737  iblitg  25744  ibl0  25763  itgcn  25821  cnlimc  25864  dvfre  25927  dvnfre  25928  dveflem  25955  dvef  25956  dvlipcn  25971  lhop2  25992  itgsubstlem  26027  deg1val  26073  ply1rem  26143  coefv0  26225  plyrecj  26258  vieta1lem2  26290  aannenlem1  26307  aaliou2b  26320  ulmval  26360  ulmpm  26363  ulmdvlem1  26380  mtest  26384  efcn  26424  sin2pim  26465  cos2pim  26466  sinmpi  26467  cosmpi  26468  sinppi  26469  cosppi  26470  efimpi  26471  sincosq1lem  26477  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  sinq12gt0  26487  sinq34lt0t  26489  sincosq1eq  26492  abssinper  26501  efif1o  26526  loglt1b  26614  relogcn  26618  ellogdm  26619  efopn  26638  cxp0  26650  cxp1  26651  cxpsqrt  26683  logsqrt  26684  logb1  26750  atandm3  26859  atanbnd  26907  atancn  26917  leibpi  26923  efrlim  26950  efrlimOLD  26951  logdifbnd  26975  vmaprm  27098  ppip1le  27142  ppieq0  27157  prmorcht  27159  ppiublem1  27184  ppiub  27186  chpeq0  27190  chtub  27194  fsumvma  27195  pclogsum  27197  chpval2  27200  dchrresb  27241  dchrptlem1  27246  lgs0  27292  lgs2  27296  lgsdir2lem2  27308  lgsdir2lem4  27310  lgsdchrval  27336  lgsdchr  27337  lgseisenlem2  27358  2lgslem1c  27375  2lgsoddprmlem2  27391  addsq2nreurex  27426  dirith2  27510  selberg2lem  27532  qabvle  27607  qabvexp  27608  ostth  27621  noextendseq  27650  noetasuplem4  27719  noetainflem4  27723  cutsun12  27801  madebdayim  27899  bdayiun  27926  addsrid  27975  addsfo  27994  peano2no  27995  negscl  28047  subsfo  28076  subsid1  28079  muls01  28123  mulsrid  28124  divs1  28215  recsex  28230  abssnid  28254  peano2ons  28291  noseqp1  28302  noseqind  28303  peano2nns  28361  n0fincut  28366  n0lts1e0  28379  dfnns2  28383  oldfib  28388  elzs2  28410  elnnzs  28412  elznns  28413  zsoring  28420  n0seo  28432  exps0  28438  exps1  28439  bdaypw2n0bndlem  28474  bdayfin  28498  istrkg2ld  28547  istrkg3ld  28548  ttgval  28962  brbtwn  28987  colinearalglem4  28997  upgr0eop  29202  uspgrushgr  29265  usgruspgr  29268  usgr0eop  29334  0grsubgr  29366  uspgrloopvtx  29604  umgr2v2evtx  29610  usgr0edg0rusgr  29664  rgrusgrprc  29678  wlkvtxiedg  29713  pthdivtx  29815  usgr2pthlem  29851  wlkswwlksf1o  29967  wwlksext2clwwlk  30147  konigsbergssiedgw  30340  frgrncvvdeqlem7  30395  2clwwlk2  30438  ex-po  30525  pliguhgr  30577  nvnd  30779  ipval2lem3  30796  ipval2  30798  ipidsq  30801  dipcj  30805  dip0r  30808  nmlnogt0  30888  blocni  30896  ipasslem2  30923  ipasslem8  30928  ipasslem9  30929  ajval  30952  ubthlem1  30961  hvaddlid  31114  hvsub0  31167  hi02  31188  hlimi  31279  isch2  31314  chlimi  31325  chsupunss  31435  shsupunss  31437  chlejb1i  31567  h1dei  31641  h1de2ci  31647  spanunsni  31670  pjoml2i  31676  pjorthi  31760  mayete3i  31819  hosubid1  31889  nmopge0  32002  nmfnge0  32018  adj1  32024  adjeq  32026  lnop0  32057  lnopmi  32091  nmophmi  32122  cnlnadjlem5  32162  cnlnadjeui  32168  unierri  32195  leoprf2  32218  leopnmid  32229  nmopleid  32230  hstles  32322  hst0  32324  strlem3a  32343  dmdbr2  32394  mdsl1i  32412  mdsl2i  32413  mdsl2bi  32414  cvmdi  32415  mdslmd1lem1  32416  mdslmd1lem2  32417  mdslmd1i  32420  mdslmd2i  32421  csmdsymi  32425  mdexchi  32426  superpos  32445  atomli  32473  atordi  32475  chirredlem1  32481  chirredlem2  32482  atcvat4i  32488  atabsi  32492  mdsymlem1  32494  mdsymlem5  32498  mdsymlem6  32499  sumdmdii  32506  dmdbr5ati  32513  dmdbr6ati  32514  mddmdin0i  32522  cdj3lem2  32526  unidifsnel  32625  unidifsnne  32626  xppreima  32738  abfmpunirn  32745  abfmpel  32748  aciunf1lem  32755  fgreu  32764  padct  32811  fpwrelmapffslem  32825  fpwrelmap  32826  xrge0infss  32853  xrdifh  32873  pfx1s2  33019  clatp0cl  33056  clatp1cl  33057  cntrcrng  33162  cycpmco2lem4  33210  rmfsupp2  33319  1fldgenq  33403  resvval  33409  rearchi  33426  qusxpid  33443  opprabs  33562  zringfrac  33634  psrbasfsupp  33692  rlmdim  33774  constrfiss  33916  2sqr3minply  33945  locfinreflem  34005  locfinref  34006  ordtconnlem1  34089  rge0scvg  34114  lmxrge0  34117  qqh0  34149  qqh1  34150  rrh0  34180  zrhre  34184  esumcst  34228  esumfzf  34234  esumfsupre  34236  hasheuni  34250  sgon  34289  dmvlsiga  34294  sigainb  34301  measval  34363  ismeas  34364  sxbrsigalem0  34436  omssubadd  34465  carsggect  34483  eulerpartlemmf  34540  eulerpartlemgs2  34545  eulerpartlemn  34546  rrvsum  34619  ballotlem2  34654  ballotlemfcc  34659  ballotlem4  34664  signsplypnf  34715  signsply0  34716  signsw0glem  34718  signswrid  34723  signlem0  34752  signshf  34753  bnj535  35053  bnj580  35076  bnj907  35130  bnj1253  35180  funen1cnv  35252  rankval4b  35264  fineqvnttrclse  35289  noinfepfnregs  35297  onvf1odlem1  35306  onvf1od  35310  loop1cycl  35340  ptpconn  35436  cvmsss2  35477  cvmlift2lem12  35517  cvmlift2lem13  35518  cvmliftphtlem  35520  cvmliftpht  35521  fmlafvel  35588  mppsthm  35782  bcneg1  35939  fv1stcnv  35980  fv2ndcnv  35981  wlimeq1  36021  imagesset  36156  altopeq1  36166  brcolinear2  36261  cldbnd  36529  ivthALT  36538  refssfne  36561  ontgval  36634  onint1  36652  ttcid  36695  ttcss  36701  ttcss2  36702  ttcsnexg  36723  ttcwf  36727  dfttc4lem2  36732  ttc0el  36738  axc11n11r  36993  bj-pm11.53a  37080  bj-bm1.3ii  37384  bj-restsn0  37410  bj-restsn10  37411  bj-restsnid  37412  bj-rest10  37413  bj-rest0  37418  bj-inftyexpiinv  37535  bj-inftyexpidisj  37537  taupilem1  37648  irrdiff  37653  f1omptsnlem  37663  mptsnunlem  37665  topdifinffinlem  37674  inunissunidif  37702  rdgssun  37705  exrecfnlem  37706  exrecfnpw  37708  finixpnum  37937  tan2h  37944  matunitlindflem2  37949  ptrest  37951  poimirlem22  37974  poimirlem25  37977  mblfinlem1  37989  mblfinlem2  37990  mblfinlem3  37991  mblfinlem4  37992  ismblfin  37993  itg2addnclem  38003  itg2addnclem2  38004  itg2addnclem3  38005  itg2addnc  38006  itg2gt0cn  38007  ftc1anclem5  38029  ftc1anclem8  38032  dvasin  38036  dvacos  38037  sdclem2  38074  totbndbnd  38121  heibor1lem  38141  heiborlem7  38149  bfplem1  38154  prnc  38399  brxrn  38715  ecxrn2  38740  dfpeters2  39306  riotasv  39416  glbconN  39834  atpointN  40200  polsubN  40364  pol0N  40366  pol1N  40367  2polvalN  40371  2polssN  40372  3polN  40373  pcl0N  40379  2pmaplubN  40383  pnonsingN  40390  polsubclN  40409  cdlemefs32sn1aw  40871  cdleme43fsv1snlem  40877  cdleme41sn3a  40890  cdleme32a  40898  cdleme40m  40924  cdleme40n  40925  cdleme42b  40935  istendo  41217  cdlemk40  41374  cdlemkid  41393  dihvalcqpre  41692  facp2  42593  relt0neg1  42912  sn-nnne0  42916  frlmsnic  42996  prjspnerlem  43061  prjspnval2  43062  0prjspn  43072  3cubes  43133  mapfzcons1cl  43161  eldioph3b  43208  eldiophss  43217  0dioph  43221  vdioph  43222  eldioph4b  43254  eldioph4i  43255  rencldnfilem  43263  rmxy1  43365  rmxy0  43366  rmxm1  43377  rmym1  43378  monotoddzzfi  43385  wepwso  43486  aomclem6  43502  pwslnmlem0  43534  isnumbasabl  43549  areaquad  43659  onexlimgt  43686  oaabsb  43737  nadd1suc  43835  oe2  43848  safesnsupfidom1o  43859  onnoxp  43875  oa1cl  43889  finona1cl  43895  reabsifneg  44074  reabsifnneg  44077  relexp2  44119  eltrclrec  44122  elrtrclrec  44123  brtrclrec  44138  brrtrclrec  44139  relexpxpmin  44159  dftrcl3  44162  dfrtrcl3  44175  heeq1  44219  seff  44751  lhe4.4ex1a  44771  eelT0  45216  snssl  45271  sineq0ALT  45378  trfr  45404  xpwf  45406  dmwf  45407  rnwf  45408  modelaxreplem1  45420  modelaxreplem3  45422  0elaxnul  45425  prclaxpr  45427  uniclaxun  45428  wfac8prim  45444  permaxinf2lem  45454  elrnmpt1sf  45634  founiiun0  45635  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  47317  natlocalincr  47319  cjnpoly  47334  sinnpoly  47336  sqrtnegnre  47752  fsummmodsnunz  47828  flsqrt5  48054  bits0ALTV  48152  mogoldbblem  48193  sgoldbeven3prm  48256  nnsum3primes4  48261  isubgr0uhgr  48346  ushggricedg  48400  2zrngnmlid  48728  2zrngnmrid  48729  mpoexxg2  48811  lco0  48900  zlmodzxzldeplem3  48975  0dig1  49082  naryfvalel  49103  ackvalsuc0val  49160  iinxp  49303  0funclem  49558  aacllem  50273