MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan2 Structured version   Visualization version   GIF version

Theorem mpan2 691
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
StepHypRef Expression
1 mpan2.1 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 mpan2.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpdan 687 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  705  mp3an23  1455  elvd  3446  elabg  3631  eueq2  3668  sbcgf  3811  sbcralg  3824  csbconstgf  3867  sbcnestgw  4375  csbnestgw  4376  sbcnestg  4380  csbnestg  4381  csbnest1g  4384  iinexg  5293  eusv2nf  5340  reusv2lem5  5347  nnullss  5410  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  6963  fvimacnvALT  7002  dff3  7045  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  8184  tpostpos2  8189  fpr3g  8227  wfr3g  8261  tfrlem10  8318  tfrlem12  8320  tfr3  8330  seqomlem1  8381  seqomlem2  8382  seqomlem4  8384  ondif2  8429  oa0  8443  om0  8444  oa1suc  8458  om1  8469  oe1  8471  oe1m  8472  omass  8507  om2  8513  oeoalem  8524  oeoelem  8526  nnmsucr  8553  nnm1  8580  nnm2  8581  naddrid  8611  naddlid  8612  ecelqs  8705  xpider  8725  mapdm0  8779  fvdiagfn  8829  ixpsnf1o  8876  xp1en  8991  undom  8993  sbthlem7  9021  domunsn  9055  xpmapenlem  9072  infensuc  9083  findcard2d  9091  diffi  9099  cnvfi  9100  enreffi  9107  snnen2o  9145  1sdom2dom  9154  infi  9170  finresfin  9172  unblem1  9192  unblem2  9193  unblem3  9194  unblem4  9195  isfinite2  9198  infn0ALT  9203  unfilem1  9205  unfilem2  9206  unfir  9208  fofinf1o  9232  cnvfiALT  9239  mptfi  9251  finsschain  9259  imafi2  9261  marypha2  9342  inf0  9530  trcl  9637  frr3g  9668  r1rankidb  9716  snwf  9721  unwf  9722  uniwf  9731  rankval3b  9738  rankr1a  9748  rankxplim3  9793  scott0  9798  djueq1  9817  card1  9880  pm54.43  9913  infxpenc2  9932  dfac8clem  9942  alephsuc2  9990  alephle  9998  cardaleph  9999  dfac12lem2  10055  undjudom  10078  djudom1  10093  pwdju1  10101  nnadju  10108  ackbij1lem18  10146  cflem  10155  cflemOLD  10156  cflecard  10163  cfeq0  10166  cfslb  10176  cfsmolem  10180  cfcoflem  10182  cfidm  10185  isfin4p1  10225  fin23lem12  10241  fin23lem16  10245  fin23lem28  10250  fin23lem38  10259  fin23lem41  10262  fin1a2lem7  10316  fin1a2lem12  10321  fin1a2lem13  10322  hsmexlem8  10334  axcc2lem  10346  axcc3  10348  domtriomlem  10352  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  ac6num  10389  ttukeylem4  10422  ttukeylem7  10425  ttukey2g  10426  axdclem  10429  brdom3  10438  brdom5  10439  cardeq0  10462  unsnen  10463  konigthlem  10479  pwcfsdom  10494  canthp1lem1  10563  wunex2  10649  wuncval2  10658  eltsk2g  10662  ingru  10726  grutsk  10733  axgroth6  10739  mulidpi  10797  nlt1pi  10817  indpi  10818  pinq  10838  mulidnq  10874  1idpr  10940  prlem934  10944  0idsr  11008  1idsr  11009  00sr  11010  negexsr  11013  recexsrlem  11014  sqgt0sr  11017  ax1rid  11072  axcnre  11075  ne0gt0  11238  peano2cn  11305  peano2re  11306  00id  11308  mul02lem2  11310  mul01  11312  subid  11400  subid1  11401  negid  11428  negeq0  11435  peano2cnm  11447  peano2rem  11448  lt0neg1  11643  le0neg1  11645  relin01  11661  div2neg  11864  recgt0ii  12048  divgt0i2i  12057  ledivp1i  12067  ltdivp1i  12068  inelr  12135  peano5nni  12148  peano2nn  12157  nnge1  12173  nnne0  12179  times2  12277  addltmul  12377  nn0p1nn  12440  peano2nn0  12441  nn0lele2xi  12457  fcdmnn0supp  12458  fcdmnn0fsupp  12459  fcdmnn0suppg  12460  peano2z  12532  peano2zm  12534  suprzcl  12572  zeo  12578  eluzaddi  12782  uzwo  12824  uzwo2  12825  infssuzle  12844  infssuzcl  12845  zq  12867  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  rphalfcl  12934  zgt1rpn0n1  12948  ltpnf  13034  nltmnf  13043  pnfge  13044  nltpnft  13079  xlemnf  13082  qsqueeze  13116  xlt0neg1  13134  xle0neg1  13136  xaddpnf1  13141  xaddmnf1  13143  xaddrid  13156  xsubge0  13176  xmul01  13182  xmulneg1  13184  xmulpnf1  13189  xmulrid  13194  supxrbnd  13243  supxrgtmnf  13244  supxrre1  13245  supxrre2  13246  elioopnf  13359  elicopnf  13361  iccshftri  13403  iccshftli  13405  iccdili  13407  icccntri  13409  fzprval  13501  fz0add1fz1  13651  fzofzp1  13680  fzostep1  13702  injresinj  13707  flge0nn0  13740  flge1nn  13741  btwnzge0  13748  modfrac  13804  om2uzsuci  13871  axdc4uzlem  13906  ser1const  13981  exp0  13988  exp1  13990  expn1  13994  nn0sqcl  14012  sqval  14037  sqeq0  14043  resqcl  14047  zsqcl  14052  expubnd  14101  binom21  14142  expnbnd  14155  nn0opthlem2  14192  bcnn  14235  bcn2  14242  bcn2p1  14248  bcnm1  14250  hasheq0  14286  hashsng  14292  hashen1  14293  hashunsnggt  14317  hashin  14334  hashdif  14336  hashgt23el  14347  hashxplem  14356  hashf1lem2  14379  hash2pr  14392  hash2prde  14393  pr2pwpr  14402  hash3tr  14414  iswrd  14438  wrdval  14439  hashwrdn  14470  ccatval2  14501  ccatrid  14511  eqs1  14536  s111  14539  ccatws1len  14544  repsw0  14700  repsw1  14706  cshw0  14717  wwlktovf  14879  relexpsucnnl  14953  reim0  15041  imval2  15074  cjne0  15086  abssq  15229  max0add  15233  abs2dif  15256  rddif  15264  absrdbnd  15265  rexuz3  15272  isershft  15587  isercolllem2  15589  isercoll  15591  fsum  15643  fsumadd  15663  fsumsplitsnun  15678  bcxmas  15758  infcvgaux2i  15781  fprod  15864  risefac0  15950  fallfac0  15951  risefac1  15956  fallfac1  15957  bpoly2  15980  bpoly3  15981  bpoly4  15982  fsumcube  15983  efi4p  16062  resin4p  16063  recos4p  16064  sinbnd  16105  cosbnd  16106  rpnnen2lem8  16146  rpnnen2lem12  16150  cnso  16172  dvdsmul2  16205  dvdslelem  16236  odd2np1lem  16267  mod2eq1n2dvds  16274  divalglem0  16320  divalglem1  16321  divalglem4  16323  divalglem5  16324  divalglem8  16327  flodddiv4  16342  bits0  16355  bitsp1o  16360  bitsf1  16373  sadadd2lem2  16377  gcd1  16455  lcm0val  16521  dvdslcm  16525  lcmeq0  16527  lcmgcd  16534  lcm1  16537  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  prm2orodd  16618  phiprm  16704  pc0  16782  pcdvdstr  16804  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  hashbc0  16933  setsval  17094  fsets  17096  setsres  17105  ressinbas  17172  ressress  17174  elrestr  17348  pwssnf1o  17419  xpsfrnel  17483  xpscf  17486  ismred2  17522  submre  17524  mreacs  17581  oppchomfval  17637  brssc  17738  isssc  17744  yonedalem4c  18200  oduleval  18212  isprs  18219  oduclatb  18430  chninf  18558  gsumval2a  18610  smndex1n0mnd  18837  mulg1  19011  mulgnegnn  19014  isghmOLD  19145  ghmghmrn  19164  cntrnsg  19273  oppgplusfval  19277  pgrpsubgsymg  19338  psgneldm2i  19434  efgrelexlemb  19679  frgp0  19689  frgpmhm  19694  vrgpf  19697  cntrcmnd  19771  cntrabl  19772  cygctb  19821  dprd0  19962  dprd2da  19973  mgpplusg  20079  opprmulfval  20275  subrngint  20493  subrgint  20528  lsp0  20960  rlmval2  21144  cncrng  21343  cnfld1  21348  zringcyg  21424  mulgrhm2  21433  zlmsca  21475  fermltlchr  21484  chrnzr  21485  zrhpsgnelbas  21549  ocvz  21633  cssincl  21643  css0  21644  css1  21645  frlmip  21733  fczpsrbag  21877  ply1idvr1OLD  22239  evls1rhmlem  22265  evl1fval1lem  22274  marrepeval  22507  decpmatid  22714  0opn  22848  topopn  22850  basdif0  22897  tgval  22899  isopn2  22976  0cld  22982  ntropn  22993  ntrval2  22995  ntrdif  22996  clsdif  22997  cmclsopn  23006  ntrtop  23014  ntr0  23025  mretopd  23036  neips  23057  neiptopnei  23076  maxlp  23091  isperf2  23096  rest0  23113  iocpnfordt  23159  icomnfordt  23160  mnfnei  23165  refref  23457  unisngl  23471  1stckgen  23498  ptbasfi  23525  pthaus  23582  fbssfi  23781  isfil2  23800  ssfg  23816  filconn  23827  fbasrn  23828  filufint  23864  imaelfm  23895  fmfnfmlem4  23901  fclsfnflim  23971  alexsubALTlem3  23993  alexsubALTlem4  23994  ustfilxp  24157  ustuqtop2  24186  ustuqtop4  24188  utopsnneiplem  24191  utopsnnei  24193  utop2nei  24194  cfiluweak  24238  neipcfilu  24239  xmetres  24308  metres  24309  mopnex  24463  prdsms  24475  metucn  24515  tngds  24592  tngngp3  24600  nmoge0  24665  cnfldnm  24722  tgioo  24740  xrtgioo  24751  xrsmopn  24757  negcncf  24871  negcncfOLD  24872  phtpy01  24940  pco0  24970  tcphtopn  25182  tchnmfval  25184  caussi  25253  rrxip  25346  minveclem3b  25384  ovolfioo  25424  ovolficc  25425  ovolfsf  25428  ovolctb  25447  ovolctb2  25449  ovolfiniun  25458  ovoliun2  25463  ovolshftlem1  25466  ovolscalem1  25470  ovolicopnf  25481  iunmbl2  25514  uniioombllem2  25540  opnmblALT  25560  ismbf  25585  mbfinf  25622  0plef  25629  itg1climres  25671  itg2cnlem1  25718  iblitg  25725  ibl0  25744  itgcn  25802  cnlimc  25845  dvfre  25911  dvnfre  25912  dveflem  25939  dvef  25940  dvlipcn  25955  lhop2  25976  itgsubstlem  26011  deg1val  26057  ply1rem  26127  coefv0  26209  plyrecj  26243  vieta1lem2  26275  aannenlem1  26292  aaliou2b  26305  ulmval  26345  ulmpm  26348  ulmdvlem1  26365  mtest  26369  efcn  26409  sin2pim  26450  cos2pim  26451  sinmpi  26452  cosmpi  26453  sinppi  26454  cosppi  26455  efimpi  26456  sincosq1lem  26462  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  sinq12gt0  26472  sinq34lt0t  26474  sincosq1eq  26477  abssinper  26486  efif1o  26511  loglt1b  26599  relogcn  26603  ellogdm  26604  efopn  26623  cxp0  26635  cxp1  26636  cxpsqrt  26668  logsqrt  26669  logb1  26735  atandm3  26844  atanbnd  26892  atancn  26902  leibpi  26908  efrlim  26935  efrlimOLD  26936  logdifbnd  26960  vmaprm  27083  ppip1le  27127  ppieq0  27142  prmorcht  27144  ppiublem1  27169  ppiub  27171  chpeq0  27175  chtub  27179  fsumvma  27180  pclogsum  27182  chpval2  27185  dchrresb  27226  dchrptlem1  27231  lgs0  27277  lgs2  27281  lgsdir2lem2  27293  lgsdir2lem4  27295  lgsdchrval  27321  lgsdchr  27322  lgseisenlem2  27343  2lgslem1c  27360  2lgsoddprmlem2  27376  addsq2nreurex  27411  dirith2  27495  selberg2lem  27517  qabvle  27592  qabvexp  27593  ostth  27606  noextendseq  27635  noetasuplem4  27704  noetainflem4  27708  cutsun12  27786  madebdayim  27884  bdayiun  27911  addsrid  27960  addsfo  27979  peano2no  27980  negscl  28032  subsfo  28061  subsid1  28064  muls01  28108  mulsrid  28109  divs1  28200  recsex  28215  abssnid  28239  peano2ons  28276  noseqp1  28287  noseqind  28288  peano2nns  28346  n0fincut  28351  n0lts1e0  28364  dfnns2  28368  oldfib  28373  elzs2  28395  elnnzs  28397  elznns  28398  zsoring  28405  n0seo  28417  exps0  28423  exps1  28424  bdaypw2n0bndlem  28459  bdayfin  28483  istrkg2ld  28532  istrkg3ld  28533  ttgval  28947  brbtwn  28972  colinearalglem4  28982  upgr0eop  29187  uspgrushgr  29250  usgruspgr  29253  usgr0eop  29319  0grsubgr  29351  uspgrloopvtx  29589  umgr2v2evtx  29595  usgr0edg0rusgr  29649  rgrusgrprc  29663  wlkvtxiedg  29698  pthdivtx  29800  usgr2pthlem  29836  wlkswwlksf1o  29952  wwlksext2clwwlk  30132  konigsbergssiedgw  30325  frgrncvvdeqlem7  30380  2clwwlk2  30423  ex-po  30510  pliguhgr  30561  nvnd  30763  ipval2lem3  30780  ipval2  30782  ipidsq  30785  dipcj  30789  dip0r  30792  nmlnogt0  30872  blocni  30880  ipasslem2  30907  ipasslem8  30912  ipasslem9  30913  ajval  30936  ubthlem1  30945  hvaddlid  31098  hvsub0  31151  hi02  31172  hlimi  31263  isch2  31298  chlimi  31309  chsupunss  31419  shsupunss  31421  chlejb1i  31551  h1dei  31625  h1de2ci  31631  spanunsni  31654  pjoml2i  31660  pjorthi  31744  mayete3i  31803  hosubid1  31873  nmopge0  31986  nmfnge0  32002  adj1  32008  adjeq  32010  lnop0  32041  lnopmi  32075  nmophmi  32106  cnlnadjlem5  32146  cnlnadjeui  32152  unierri  32179  leoprf2  32202  leopnmid  32213  nmopleid  32214  hstles  32306  hst0  32308  strlem3a  32327  dmdbr2  32378  mdsl1i  32396  mdsl2i  32397  mdsl2bi  32398  cvmdi  32399  mdslmd1lem1  32400  mdslmd1lem2  32401  mdslmd1i  32404  mdslmd2i  32405  csmdsymi  32409  mdexchi  32410  superpos  32429  atomli  32457  atordi  32459  chirredlem1  32465  chirredlem2  32466  atcvat4i  32472  atabsi  32476  mdsymlem1  32478  mdsymlem5  32482  mdsymlem6  32483  sumdmdii  32490  dmdbr5ati  32497  dmdbr6ati  32498  mddmdin0i  32506  cdj3lem2  32510  unidifsnel  32610  unidifsnne  32611  xppreima  32723  abfmpunirn  32730  abfmpel  32733  aciunf1lem  32740  fgreu  32750  padct  32797  fpwrelmapffslem  32811  fpwrelmap  32812  xrge0infss  32840  xrdifh  32860  indconst0  32939  indconst1  32940  pfx1s2  33021  clatp0cl  33058  clatp1cl  33059  cntrcrng  33163  cycpmco2lem4  33211  rmfsupp2  33320  1fldgenq  33404  resvval  33410  rearchi  33427  qusxpid  33444  opprabs  33563  zringfrac  33635  psrbasfsupp  33693  rlmdim  33766  constrfiss  33908  2sqr3minply  33937  locfinreflem  33997  locfinref  33998  ordtconnlem1  34081  rge0scvg  34106  lmxrge0  34109  qqh0  34141  qqh1  34142  rrh0  34172  zrhre  34176  esumcst  34220  esumfzf  34226  esumfsupre  34228  hasheuni  34242  sgon  34281  dmvlsiga  34286  sigainb  34293  measval  34355  ismeas  34356  sxbrsigalem0  34428  omssubadd  34457  carsggect  34475  eulerpartlemmf  34532  eulerpartlemgs2  34537  eulerpartlemn  34538  rrvsum  34611  ballotlem2  34646  ballotlemfcc  34651  ballotlem4  34656  signsplypnf  34707  signsply0  34708  signsw0glem  34710  signswrid  34715  signlem0  34744  signshf  34745  bnj535  35046  bnj580  35069  bnj907  35123  bnj1253  35173  funen1cnv  35244  rankval4b  35256  fineqvnttrclse  35280  noinfepfnregs  35288  onvf1odlem1  35297  onvf1od  35301  loop1cycl  35331  ptpconn  35427  cvmsss2  35468  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmliftphtlem  35511  cvmliftpht  35512  fmlafvel  35579  mppsthm  35773  bcneg1  35930  fv1stcnv  35971  fv2ndcnv  35972  wlimeq1  36012  imagesset  36147  altopeq1  36157  brcolinear2  36252  cldbnd  36520  ivthALT  36529  refssfne  36552  ontgval  36625  onint1  36643  axc11n11r  36884  bj-pm11.53a  36979  bj-bm1.3ii  37265  bj-restsn0  37290  bj-restsn10  37291  bj-restsnid  37292  bj-rest10  37293  bj-rest0  37298  bj-inftyexpiinv  37413  bj-inftyexpidisj  37415  taupilem1  37526  irrdiff  37531  f1omptsnlem  37541  mptsnunlem  37543  topdifinffinlem  37552  inunissunidif  37580  rdgssun  37583  exrecfnlem  37584  exrecfnpw  37586  finixpnum  37806  tan2h  37813  matunitlindflem2  37818  ptrest  37820  poimirlem22  37843  poimirlem25  37846  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  ftc1anclem5  37898  ftc1anclem8  37901  dvasin  37905  dvacos  37906  sdclem2  37943  totbndbnd  37990  heibor1lem  38010  heiborlem7  38018  bfplem1  38023  prnc  38268  brxrn  38568  ecxrn2  38593  riotasv  39219  glbconN  39637  atpointN  40003  polsubN  40167  pol0N  40169  pol1N  40170  2polvalN  40174  2polssN  40175  3polN  40176  pcl0N  40182  2pmaplubN  40186  pnonsingN  40193  polsubclN  40212  cdlemefs32sn1aw  40674  cdleme43fsv1snlem  40680  cdleme41sn3a  40693  cdleme32a  40701  cdleme40m  40727  cdleme40n  40728  cdleme42b  40738  istendo  41020  cdlemk40  41177  cdlemkid  41196  dihvalcqpre  41495  facp2  42397  relt0neg1  42711  sn-nnne0  42715  frlmsnic  42795  prjspnerlem  42860  prjspnval2  42861  0prjspn  42871  3cubes  42932  mapfzcons1cl  42960  eldioph3b  43007  eldiophss  43016  0dioph  43020  vdioph  43021  eldioph4b  43053  eldioph4i  43054  rencldnfilem  43062  rmxy1  43164  rmxy0  43165  rmxm1  43176  rmym1  43177  monotoddzzfi  43184  wepwso  43285  aomclem6  43301  pwslnmlem0  43333  isnumbasabl  43348  areaquad  43458  onexlimgt  43485  oaabsb  43536  nadd1suc  43634  oe2  43647  safesnsupfidom1o  43658  onnoxp  43674  oa1cl  43688  finona1cl  43694  reabsifneg  43873  reabsifnneg  43876  relexp2  43918  eltrclrec  43921  elrtrclrec  43922  brtrclrec  43937  brrtrclrec  43938  relexpxpmin  43958  dftrcl3  43961  dfrtrcl3  43974  heeq1  44018  seff  44550  lhe4.4ex1a  44570  eelT0  45015  snssl  45070  sineq0ALT  45177  trfr  45203  xpwf  45205  dmwf  45206  rnwf  45207  modelaxreplem1  45219  modelaxreplem3  45221  0elaxnul  45224  prclaxpr  45226  uniclaxun  45227  wfac8prim  45243  permaxinf2lem  45253  elrnmpt1sf  45433  founiiun0  45434  supxrgere  45578  supxrgelem  45582  fmuldfeqlem1  45828  fmuldfeq  45829  climneg  45856  sumnnodd  45876  liminfltlem  46048  xlimpnfxnegmnf2  46102  addccncf2  46120  dvsinax  46157  stoweidlem18  46262  stoweidlem19  46263  stoweidlem22  46266  stoweidlem34  46278  stoweidlem40  46284  stoweidlem41  46285  stoweidlem55  46299  stoweidlem59  46303  dirker2re  46336  dirkerdenne0  46337  fourierdlem48  46398  fourierdlem49  46399  fourierdlem70  46420  fourierdlem71  46421  fourierdlem104  46454  fourierdlem112  46462  fouriersw  46475  etransclem46  46524  etransclem48  46526  nnfoctbdjlem  46699  ormklocald  47118  natlocalincr  47120  cjnpoly  47135  sinnpoly  47137  sqrtnegnre  47553  fsummmodsnunz  47621  flsqrt5  47840  bits0ALTV  47925  mogoldbblem  47966  sgoldbeven3prm  48029  nnsum3primes4  48034  isubgr0uhgr  48119  ushggricedg  48173  2zrngnmlid  48501  2zrngnmrid  48502  mpoexxg2  48584  lco0  48673  zlmodzxzldeplem3  48748  0dig1  48855  naryfvalel  48876  ackvalsuc0val  48933  iinxp  49076  0funclem  49331  aacllem  50046
  Copyright terms: Public domain W3C validator