MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2antlr Structured version   Unicode version

Theorem ad2antlr 725
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antlr  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 463 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 712 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  ad3antlr  729  simplr  754  simplrl  762  simplrr  763  frsn  4894  sofld  5272  foun  5817  f1oprg  5839  fvreseq1  5966  fpr2g  6112  foeqcnvco  6186  f1eqcocnv  6187  caovord3  6469  tfindsg  6678  soex  6727  curry1  6876  curry2  6879  f1o2ndf1  6892  suppfnss  6928  mpt2xopxnop0  6946  smores2  7058  smo11  7068  smoord  7069  oesuclem  7212  oelim  7221  oaordi  7232  oaass  7247  odi  7265  omass  7266  oen0  7272  oelim2  7281  nnaordi  7304  eceqoveq  7453  resixpfo  7545  boxcutc  7550  xpdom2  7650  domunsncan  7655  omxpenlem  7656  mapen  7719  xpmapenlem  7722  mapdom2  7726  php3  7741  onomeneq  7745  fineqvlem  7769  xpfi  7825  fiint  7831  dffi3  7925  marypha1lem  7927  ordtypelem7  7983  wemaplem3  8007  brwdom2  8033  unxpwdom2  8048  cantnfle  8122  cantnflt  8123  cantnfleOLD  8152  cantnfltOLD  8153  r1pwss  8234  rankval3b  8276  carddomi2  8383  isinffi  8405  fidomtri  8406  acndom  8464  dfac9  8548  dfac12lem1  8555  dfac12lem2  8556  ackbij1lem16  8647  ackbij2lem3  8653  fictb  8657  cofsmo  8681  cfsmolem  8682  cfcof  8686  infpssrlem4  8718  fin23lem39  8762  isf32lem2  8766  isf32lem3  8767  fin1a2lem12  8823  fin1a2lem13  8824  fin12  8825  axdc3lem4  8865  axdc4lem  8867  ttukeylem3  8923  carden  8958  axrepnd  9001  canthwelem  9058  inawinalem  9097  gchina  9107  r1limwun  9144  inar1  9183  inatsk  9186  tskuni  9191  intgru  9222  nqereu  9337  ltexnq  9383  npex  9394  elnp  9395  prlem936  9455  recexsrlem  9510  mul02lem1  9790  lemul12a  10441  mulge0b  10453  lediv12a  10478  lediv2a  10479  creur  10570  peano5nni  10579  nndiv  10617  rpnnen1lem1  11253  rpnnen1lem2  11254  rpnnen1lem3  11255  rpnnen1lem5  11257  xrmax2  11430  qextltlem  11454  xpncan  11496  xmulneg1  11514  xmulge0  11529  xlemul1a  11533  xrsupsslem  11551  xrinfmsslem  11552  xrub  11556  supxrun  11560  supxrunb1  11564  supxrunb2  11565  supxrbnd  11573  ixxub  11603  ixxlb  11604  elioc2  11641  elico2  11642  elicc2  11643  difreicc  11706  elfznelfzo  11952  flflp1  11981  modid  12059  modaddmodup  12091  modaddmodlo  12092  seqf1olem1  12190  facndiv  12410  faclbnd  12412  bcval5  12440  hashdom  12495  hashfacen  12552  seqcoll  12561  brfi1indlem  12580  brfi1uzind  12581  ccatw2s1p2  12695  revccat  12796  cshwsexa  12848  2cshwcshw  12849  cshwcsh2id  12852  seqshft  13067  sqrmo  13234  absmax  13311  rexico  13335  cau3lem  13336  limsupval2  13452  rlim2lt  13469  o1lo1  13509  rlimconst  13516  climrlim2  13519  2clim  13544  rlimcn2  13562  reccn2  13568  cn1lem  13569  o1of2  13584  lo1const  13592  climsqz  13612  climsqz2  13613  isercolllem2  13637  isercoll  13639  climsup  13641  climcau  13642  caucvgrlem2  13646  iseralt  13656  sumeq2ii  13664  fsum2dlem  13736  fsum0diag2  13749  cvgcmp  13781  cvgcmpce  13783  climcnds  13814  divrcnv  13815  mertenslem1  13845  mertens  13847  ntrivcvg  13858  prodeq2ii  13872  fprod2dlem  13936  efaddlem  14037  tanaddlem  14110  sqrt2irr  14191  dvdseq  14242  dvdsext  14246  odd2np1  14255  bitsf1  14305  smuval2  14341  qredeq  14456  qredeu  14457  exprmfct  14460  isprm5  14462  rpexp1i  14471  nonsq  14501  powm2modprm  14537  iserodd  14568  pcz  14613  fldivp1  14625  pcfac  14627  expnprm  14630  prmpwdvds  14631  prmreclem5  14647  vdwapf  14699  vdwnnlem2  14723  0ramcl  14750  cshwsidrepswmod0  14788  cshwshashlem1  14789  cshwshash  14798  setscom  14873  firest  15047  isacs2  15267  mreacs  15272  acsfn  15273  acsfn1  15275  ressffth  15551  setcmon  15690  funcestrcsetclem9  15741  funcsetcestrclem9  15756  uncfcurf  15832  drsdirfi  15891  resmhm  16314  resmhm2  16315  mhmco  16317  pwsdiagmhm  16324  gsumwsubmcl  16330  gsumwmhm  16337  gsumwspan  16338  isgrpinv  16424  mulgz  16487  grpissubg  16545  resghm  16607  cntzsubm  16697  cntzmhm  16700  gsmsymgreqlem2  16780  symgfixf1  16786  f1omvdconj  16795  f1otrspeq  16796  f1omvdco2  16797  symggen  16819  odf1  16908  gexdvds  16928  pgpfi  16949  sylow3lem6  16976  lsmub1x  16990  lsmless12  17005  efgred2  17095  efgcpbllemb  17097  torsubg  17184  prmcyg  17220  ghmcyg  17222  gsumval3OLD  17232  telgsums  17342  dprdfadd  17380  dprdfaddOLD  17387  subgdmdprd  17401  dprdsn  17403  dmdprdsplitlem  17404  dmdprdsplitlemOLD  17405  dmdprdsplit2lem  17414  ablfacrp  17437  ablfac1b  17441  ablfac2  17460  mgpress  17472  irredrmul  17676  isdrng2  17726  drngmul0or  17737  issubdrg  17774  islss3  17925  lmhmco  18009  lmhmplusg  18010  pwsdiaglmhm  18023  lvecvs0or  18074  lbsextlem2  18125  2idlcpbl  18202  issubassa2  18314  evlslem3  18503  evlseu  18505  evlsval  18508  coe1tmmul2  18637  coe1tmmul  18638  qsssubdrg  18797  prmirredlem  18830  mulgrhm2  18836  znidomb  18898  znunit  18900  cyggic  18909  evpmodpmf1o  18930  psgndiflemA  18935  pjfo  19044  obslbs  19059  uvcff  19118  lindfmm  19154  islinds4  19162  matassa  19238  mat1dimscm  19269  mat1dimcrng  19271  mat1mhm  19278  dmatmul  19291  1marepvmarrepid  19369  mdetleib2  19382  madutpos  19436  matunit  19472  cramer0  19484  mat2pmatghm  19523  mat2pmatmul  19524  mat2pmat1  19525  mat2pmatlin  19528  mat2pmatscmxcl  19533  monmatcollpw  19572  pmatcollpw3fi1lem1  19579  pmatcollpwscmatlem1  19582  pm2mpf1  19592  mp2pm2mplem4  19602  pm2mpghm  19609  chpscmat  19635  chpscmatgsumbin  19637  chfacffsupp  19649  chfacfscmul0  19651  chfacfscmulfsupp  19652  chfacfscmulgsum  19653  chfacfpmmul0  19655  chfacfpmmulfsupp  19656  chfacfpmmulgsum  19657  cayhamlem4  19681  tgdom  19772  fctop  19797  pptbas  19801  elcls3  19877  toponmre  19887  neiptopuni  19924  neiptoptop  19925  neiptopreu  19927  maxlp  19941  ssrest  19970  cnfval  20027  cnpfval  20028  iscnp3  20038  subbascn  20048  ssidcn  20049  cnpnei  20058  cncls2  20067  cncls  20068  cnntr  20069  cncnp  20074  restcnrm  20156  cmpsublem  20192  cmpsub  20193  cmpcld  20195  uncmp  20196  hauscmplem  20199  cmpfi  20201  iunconlem  20220  2ndcrest  20247  2ndcctbss  20248  2ndcomap  20251  2ndcsep  20252  1stcelcls  20254  lly1stc  20289  lfinpfin  20317  lfinun  20318  dissnref  20321  1stckgenlem  20346  ptval  20363  ptbasfi  20374  txcls  20397  tx1cn  20402  ptclsg  20408  xkoccn  20412  upxp  20416  xkococnlem  20452  imasnopn  20483  imasncld  20484  imasncls  20485  tgqtop  20505  qtopcld  20506  reghmph  20586  ptcmpfi  20606  filcon  20676  fbasrn  20677  filuni  20678  isufil2  20701  ssufl  20711  ufileu  20712  filufint  20713  ufilen  20723  rnelfm  20746  flimopn  20768  flimclsi  20771  hauspwpwf1  20780  isfcls  20802  fcfval  20826  alexsublem  20836  alexsubALTlem2  20840  alexsubALTlem3  20841  alexsubALTlem4  20842  ptcmplem2  20845  ptcmplem3  20846  cnextfval  20854  symgtgp  20892  opnsubg  20898  clsnsg  20900  tsmsresOLD  20937  tsmsres  20938  tsmsf1o  20939  restutopopn  21033  neipcfilu  21091  stdbdmet  21311  metcnp  21336  metustidOLD  21354  metustid  21355  metustsymOLD  21356  metustsym  21357  metustblOLD  21375  metustbl  21376  metutopOLD  21377  psmetutop  21378  isngp2  21409  subgngp  21441  ngptgp  21442  tngtopn  21456  sranlm  21485  nlmvscn  21488  nmo0  21534  nmoco  21536  qdensere  21569  iocopnst  21732  oprpiece1res2  21744  evth2  21752  xlebnum  21757  lebnumii  21758  pcoass  21816  nmoleub2lem3  21890  nmhmcn  21895  lmnn  21994  cfilfcls  22005  iscmet3lem1  22022  iscmet3lem2  22023  causs  22029  equivcfil  22030  lmclim  22033  lmcau  22043  flimcfil  22044  cmetss  22045  relcmpcmet  22047  bcthlem4  22058  bcthlem5  22059  minveclem3  22136  ovoliunlem2  22206  ovolicc2lem4  22223  nulmbl2  22239  iundisj  22250  ioombl1lem4  22263  vitalilem1  22309  vitali  22314  mbfconstlem  22328  mbfimaicc  22332  mbfimaopnlem  22354  mbfsup  22363  i1fd  22380  i1fmullem  22393  i1fadd  22394  itg1addlem4  22398  itg1addlem5  22399  i1fres  22404  itg10a  22409  itg1climres  22413  mbfi1fseqlem3  22416  mbfi1fseqlem4  22417  mbfi1fseqlem5  22418  itg2const2  22440  itg2seq  22441  itg2monolem1  22449  itg2mono  22452  itg2i1fseqle  22453  itg2cnlem1  22460  iblitg  22467  ibl0  22485  itgss  22510  itgeqa  22512  iblabsr  22528  iblmulc2  22529  bddmulibl  22537  dvnff  22618  dvcobr  22641  dvrec  22650  dvmptfsum  22668  dvexp3  22671  c1liplem1  22689  c1lip1  22690  dvgt0lem1  22695  tdeglem4  22750  ply1divex  22829  q1pval  22846  fta1g  22860  plyco0  22881  plyeq0lem  22899  plymullem1  22903  plyco  22930  coemullem  22939  coemulhi  22943  coemulc  22944  coe1termlem  22947  dgrlt  22955  dgrco  22964  plycjlem  22965  dvply1  22972  plydivex  22985  fta1  22996  aalioulem2  23021  aalioulem3  23022  aalioulem6  23025  aaliou  23026  taylfval  23046  ulmcaulem  23081  ulmcau  23082  itgulm  23095  pserdvlem2  23115  pilem2  23139  divlogrlim  23310  logcnlem5  23321  advlogexp  23330  cxpcn3  23418  atantayl2  23594  leibpi  23598  birthdaylem3  23609  rlimcnp  23621  cxplim  23627  cxploglim2  23634  ftalem3  23729  basellem2  23736  mumullem1  23834  sqff1o  23837  muinv  23850  chtublem  23867  vmasum  23872  logfac2  23873  mersenne  23883  dchrptlem1  23920  bposlem1  23940  bposlem3  23942  bposlem5  23944  lgslem4  23955  lgsval2lem  23962  lgsmod  23977  lgsdir2lem4  23982  lgsdinn0  23996  lgsquad2lem2  24015  lgsquad3  24017  2sqlem6  24025  2sqlem7  24026  dchrisumlem3  24057  dchrmusumlema  24059  dchrmusum2  24060  dchrvmasumlem1  24061  dchrvmasum2lem  24062  dchrvmasumlem2  24064  dchrvmasumiflem1  24067  dchrisum0lema  24080  dchrisum0lem2a  24083  dchrisum0lem2  24084  mulog2sumlem2  24101  selberg  24114  pntsval2  24142  pntibnd  24159  pntlem3  24175  ostthlem1  24193  ostth2lem2  24200  ostth3  24204  brbtwn2  24625  colinearalglem4  24629  colinearalg  24630  axsegconlem8  24644  axsegconlem9  24645  axsegconlem10  24646  ax5seglem3  24651  ax5seglem5  24653  axbtwnid  24659  axlowdimlem17  24678  axeuclid  24683  axcontlem2  24685  axcontlem7  24690  axcontlem8  24691  usgrares1  24827  nbgraf1olem1  24858  nb3graprlem1  24868  cusgrasize2inds  24894  cusgrafilem2  24897  2wlklem1  25016  constr2wlk  25017  usgra2wlkspthlem1  25036  constr3trl  25076  constr3pth  25077  constr3cycl  25078  wwlkn0s  25122  wwlknext  25141  wwlknextbi  25142  wwlkextfun  25146  wwlkextproplem3  25160  clwwlkn2  25192  clwlkisclwwlklem2a4  25201  clwwlkf1  25213  wwlkext2clwwlk  25220  clwwisshclwwlem  25223  erclwwlkeqlen  25229  erclwwlksym  25231  erclwwlktr  25232  erclwwlkneqlen  25241  eleclclwwlkn  25250  hashecclwwlkn1  25251  usghashecclwwlk  25252  clwlkfclwwlk  25261  clwlkf1clwwlk  25267  el2spthonot0  25288  usgravd0nedg  25335  cusgraisrusgra  25355  rusgranumwlklem0  25365  rusgranumwlks  25373  iseupa  25382  eupath2  25397  frgra2v  25416  2pthfrgra  25428  frgrancvvdeqlem3  25449  frgrancvvdeqlemC  25456  frgrancvvdeqlem9  25458  frg2woteu  25472  frg2woteq  25477  extwwlkfablem2  25495  numclwwlkovf2ex  25503  numclwwlk1  25515  numclwwlk2lem1  25519  frgrareg  25534  grpoidinv  25624  grpoideu  25625  nvmul0or  25961  vacn  26018  smcnlem  26021  nmoub3i  26102  nmoo0  26120  blocnilem  26133  ubthlem1  26200  ubthlem2  26201  ubthlem3  26202  minvecolem3  26206  hvmul0or  26356  hvmulcan  26403  hvaddsub4  26409  his35  26419  occon  26619  ocorth  26623  occl  26636  chscllem2  26970  5oalem1  26986  5oalem2  26987  3oalem2  26995  pjds3i  27045  nmopub2tALT  27241  nmfnleub2  27258  hmopadj2  27273  0cnop  27311  0cnfn  27312  nmophmi  27363  cnlnadjlem6  27404  leopnmid  27470  nmopleid  27471  opsqrlem1  27472  pjss2coi  27496  pjssdif1i  27507  pj3cor1i  27541  mdsl0  27642  mdslmd1lem1  27657  mdslmd1lem2  27658  csmdsymi  27666  superpos  27686  atomli  27714  chirredlem2  27723  chirredlem3  27724  atcvat3i  27728  atcvat4i  27729  mdsymlem5  27739  cdjreui  27764  cdj1i  27765  foresf1o  27818  rabfodom  27819  disjdifprg  27867  iundisjf  27881  fcnvgreu  27957  fpwrelmap  28003  xaddeq0  28014  iundisjfi  28049  ishashinf  28057  xrsmulgzz  28118  xrge0adddir  28134  abliso  28138  submomnd  28152  ofldchr  28257  suborng  28258  locfinreflem  28296  pcmplfinf  28317  xrge0iifiso  28370  pnfneige0  28386  lmxrge0  28387  gsumesum  28506  esumlub  28507  esumcst  28510  esumrnmpt2  28515  esum2dlem  28539  esum2d  28540  insiga  28585  ldgenpisyslem1  28611  measinb  28669  cntmeas  28674  imambfm  28710  omsf  28744  omssubadd  28748  carsgclctunlem3  28768  carsgsiga  28770  omsmeas  28771  eulerpartlemgvv  28821  rrvsum  28899  ballotlemsv  28954  ballotlemsima  28960  plymulx0  29010  signsplypnf  29013  signsply0  29014  signswmnd  29020  bnj1098  29169  bnj1118  29367  bnj1417  29424  derangenlem  29468  subfacp1lem6  29482  conpcon  29532  txscon  29538  mrsubrn  29725  msubco  29743  fundmpss  29980  dftrpred3g  30047  poseq  30064  soseq  30065  sltval2  30116  nobndlem6  30157  finminlem  30546  nn0prpwlem  30550  neibastop3  30590  fgmin  30598  fin2so  31412  mblfinlem2  31424  mblfinlem3  31425  ismblfin  31427  cnambfre  31435  itg2addnclem  31439  itg2addnclem2  31440  itg2addnclem3  31441  itg2addnc  31442  itg2gt0cn  31443  iblabsnclem  31451  iblmulc2nc  31453  ftc1cnnc  31462  ftc1anclem5  31467  ftc1anclem6  31468  ftc1anclem7  31469  ftc1anclem8  31470  ftc1anc  31471  filbcmb  31513  sdclem1  31518  fdc  31520  nnubfi  31525  nninfnub  31526  geomcau  31534  istotbnd3  31549  sstotbnd3  31554  isbnd3  31562  ssbnd  31566  prdsbnd  31571  cntotbnd  31574  heiborlem8  31596  bfplem2  31601  rrncmslem  31610  rngoisocnv  31666  unichnidl  31710  keridl  31711  prnc  31746  ax12eq  31964  ax12el  31965  cvrval5  32432  3dim0  32474  pmapglbx  32786  pclfinclN  32967  lhplt  33017  lhpexle1  33025  lhpocnle  33033  lhpjat1  33037  lhpjat2  33038  lhpj1  33039  lhpmcvr  33040  lhpmcvr2  33041  lhpm0atN  33046  lhpmat  33047  ltrnid  33152  trlcl  33182  trlle  33202  cdlemc4  33212  cdleme0cp  33232  cdleme0cq  33233  cdlemeulpq  33238  cdleme1b  33244  cdleme1  33245  cdleme2  33246  cdleme3b  33247  cdleme3c  33248  cdlemedb  33315  cdleme27a  33386  docaclN  34144  doca2N  34146  djajN  34157  dihglblem5apreN  34311  elrfirn  34989  isnacs3  35004  mzpsubmpt  35037  mzprename  35043  lzunuz  35062  eldiophss  35069  eqrabdioph  35072  rexrabdioph  35089  rabdiophlem2  35097  ctbnfien  35113  irrapxlem1  35119  irrapxlem2  35120  irrapxlem4  35122  pell1234qrreccl  35151  pell1234qrmulcl  35152  pell14qrgt0  35156  pell1234qrdich  35158  pell1qrgaplem  35170  pellqrex  35176  reglogltb  35188  reglogleb  35189  monotoddzzfi  35239  oddcomabszz  35241  jm2.24  35262  congsym  35267  acongtr  35277  acongrep  35279  jm2.18  35292  jm2.23  35300  jm2.26a  35304  jm2.26lem3  35305  jm2.27b  35310  rmydioph  35318  setindtr  35328  wepwsolem  35349  dnnumch1  35352  fnwe2lem2  35359  aomclem6  35367  dfac21  35374  islssfg  35378  lnmlsslnm  35389  pwslnm  35402  lnrfg  35432  dgrsub2  35448  mpaaeu  35463  rngunsnply  35486  acsfn1p  35512  cntzsdrg  35515  idomodle  35517  prmunb2  36039  isprm7  36040  radcnvrat  36043  dvdslcm  36052  lcmneg  36057  lcmgcdlem  36060  binomcxplemfrat  36104  binomcxplemradcnv  36105  binomcxplemnotnn0  36109  fzdifsuc2  36881  fmuldfeqlem1  36944  fmuldfeq  36945  mccl  36974  climrec  36977  climinf  36980  climsuse  36982  limciccioolb  36995  constlimc  36998  limcrecl  37003  sumnnodd  37004  lptioo2  37005  lptioo1  37006  limcicciooub  37011  islpcn  37013  limsupre  37015  limcresiooub  37016  limcresioolb  37017  0ellimcdiv  37023  icccncfext  37058  fperdvper  37083  dvbdfbdioolem2  37094  dvnmptdivc  37103  dvnxpaek  37107  dvnmul  37108  dvmptfprod  37110  dvnprodlem1  37111  dvnprodlem2  37112  dvnprodlem3  37113  itgsinexp  37121  iblsplit  37133  iblspltprt  37140  itgioocnicc  37144  iblcncfioo  37145  itgspltprt  37146  stoweidlem3  37153  stoweidlem7  37157  stoweidlem14  37164  stoweidlem29  37179  stoweidlem34  37184  stoweidlem44  37194  stoweidlem46  37196  dirkerper  37246  dirkertrigeq  37251  dirkeritg  37252  dirkercncflem1  37253  dirkercncflem2  37254  dirkercncf  37257  fourierdlem12  37269  fourierdlem15  37272  fourierdlem17  37274  fourierdlem34  37291  fourierdlem35  37292  fourierdlem41  37298  fourierdlem42  37299  fourierdlem43  37300  fourierdlem46  37303  fourierdlem47  37304  fourierdlem48  37305  fourierdlem49  37306  fourierdlem50  37307  fourierdlem51  37308  fourierdlem63  37320  fourierdlem64  37321  fourierdlem65  37322  fourierdlem66  37323  fourierdlem71  37328  fourierdlem72  37329  fourierdlem73  37330  fourierdlem79  37336  fourierdlem81  37338  fourierdlem82  37339  fourierdlem83  37340  fourierdlem87  37344  fourierdlem97  37354  fourierdlem101  37358  fourierdlem102  37359  fourierdlem103  37360  fourierdlem104  37361  fourierdlem111  37368  fourierdlem114  37371  fourierswlem  37381  fouriersw  37382  elaa2lem  37384  elaa2  37385  etransclem17  37402  etransclem24  37409  etransclem25  37410  etransclem27  37412  etransclem32  37417  etransclem35  37420  2reu4a  37562  funressnfv  37581  mod2eq1n2dvds  37676  iccpartgt  37694  perfectALTV  37798  bgoldbtbndlem2  37854  bgoldbtbnd  37857  f1dmvrnfibi  37945  usgra2pthlem1  37982  issubmgm2  38107  resmgmhm  38115  resmgmhm2  38116  mgmhmco  38118  isrng  38193  zrrnghm  38234  uzlidlring  38246  rngcinv  38300  rngcinvALTV  38312  ringcinv  38351  funcringcsetcALTV2lem9  38363  ringcinvALTV  38375  funcringcsetclem9ALTV  38386  lcosslsp  38550  ldepspr  38585  nno  38648  fllog2  38699  nnolog2flm1  38721
  Copyright terms: Public domain W3C validator