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

Theorem biimpi 199
Description: Infer an implication from a logical equivalence. Inference associated with biimp 198. (Contributed by NM, 29-Dec-1992.)
Hypothesis
Ref Expression
biimpi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpi  |-  ( ph  ->  ps )

Proof of Theorem biimpi
StepHypRef Expression
1 biimpi.1 . 2  |-  ( ph  <->  ps )
2 biimp 198 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  sylbi  200  sylib  201  sylbb  202  biimpri  211  mpbi  213  syl5bi  225  syl6ib  234  syl7bi  238  syl8ib  239  pm2.53  379  simplbi  466  simprbi  470  sylanb  479  sylan2b  482  pm3.1  505  orbi2i  526  pm2.32  533  anc2l  562  pm3.37  587  dfbi  639  pm2.76  864  pm5.15  905  pm5.16  906  pm5.75  953  pm5.75OLD  954  rnlemOLD  982  simp1bi  1029  simp2bi  1030  simp3bi  1031  syl3an1b  1312  syl3an2b  1313  syl3an3b  1314  nic-ax  1567  19.25  1754  stdpc5vOLD  1799  sbbii  1815  spvw  1825  excomim  1940  stdpc5  2001  sb9i  2267  exmoeu  2342  2mo  2391  eqeq1d  2464  gencbvex  3104  moeq  3226  euind  3237  reuind  3255  eqsbc3r  3336  ra4v  3364  ra4  3366  ssel  3438  elunnel1  3587  unssd  3622  ssind  3668  n0moeu  3757  ss0  3777  uneqdifeq  3868  rabsnif  4054  prprc  4097  ssunsn2  4144  eqsn  4146  preqr1  4161  unisn2  4553  snexALT  4603  reusv3i  4624  snex  4655  elopabr  4752  brrelex12  4891  elrel  4956  exopxfr2  4998  dmxp  5072  xpssres  5158  elres  5159  elimasni  5214  inisegn0  5219  xpdifid  5284  dmsnsnsn  5333  coi2  5371  xpco  5395  iotabi  5574  uniabio  5575  iotaint  5578  nfunv  5632  funun  5643  funcnv3  5666  funimass1  5678  funssxp  5765  f0dom0  5790  f1o00  5870  dffv3  5884  dffv2  5961  fndmin  6012  iinpreima  6033  fveqressseq  6041  fsn2  6086  ftpg  6098  f12dfv  6197  f13dfv  6198  nvocnv  6205  isoselem  6257  riotaxfrd  6307  oprabid  6342  mpt2difsnif  6416  ovima0  6475  sorpsscmpl  6609  unexg  6619  ordsson  6643  peano2  6740  1stval  6822  2ndval  6823  1stdm  6867  oprabco  6907  f1o2ndf1  6931  poxp  6935  suppval1  6947  funsssuppss  6968  fnsuppeq0  6970  imacosupp  6982  wfrlem4  7065  wfrlem5  7066  wfrlem10  7071  wfrlem15  7076  tz7.49c  7189  undifixp  7584  bren2  7626  ensym  7644  en1uniel  7667  domunsn  7748  limenpsi  7773  php4  7785  snnen2o  7787  isinf  7811  en2  7833  findcard2  7837  unfilem1  7861  suppssfifsupp  7924  fsuppunbi  7930  elfiun  7970  marypha1lem  7973  marypha2lem3  7977  supval2  7995  supmaxlemOLD  8008  eqinf  8026  brwdom2  8114  brwdom3  8123  sucprcreg  8140  preleq  8148  tcmin  8251  prwf  8308  r1pw  8342  rankuni2b  8350  rankr1id  8359  cardval3  8412  ficardom  8421  cardmin2  8458  isinfcard  8549  iscard3  8550  alephval3  8567  dfac9  8592  kmlem6  8611  ackbij1lem12  8687  fin23lem29  8797  fin23lem30  8798  fin23lem41  8808  isf32lem11  8819  isfin1-3  8842  fin1a2lem11  8866  fin1a2lem12  8867  fin1a2lem13  8868  axcc2lem  8892  dominf  8901  axdc4lem  8911  dominfac  9024  pwcfsdom  9034  cfpwsdom  9035  tskuni  9234  wfgru  9267  rpregt0  11344  supxrun  11630  elicore  11716  xrge0neqmnf  11766  elfz1end  11858  1fv  11939  elfzonlteqm1  12020  fzennn  12213  cardfz  12215  fsuppmapnn0fiubex  12236  fsuppmapnn0fiub0  12237  ser0  12297  crreczi  12429  faclbnd  12507  bcn1  12530  hashrabsn01  12584  hashge0  12598  prsshashgt1  12619  hashssdif  12621  hashdifpr  12624  hashsnlei  12625  hashpw  12641  ccatw2s1p1  12806  swrd0len0  12829  swrdtrcfv  12834  swrdswrd  12853  swrdccatwrd  12861  swrdccatin2  12880  swrdccat3  12885  swrdccat3a  12887  repsundef  12911  cshwlen  12938  s4f1o  13049  trclublem  13108  reltrclfv  13130  dmtrclfv  13131  relexpsucnnr  13137  sqrt0  13354  cau3lem  13466  harmonic  13966  mertenslem2  13990  prodf1  13996  fprodfac  14076  fprodle  14099  risefacp1  14131  fallfacp1  14132  rpnnen2  14327  lcmcllem  14610  lcmftp  14658  lcmfunsnlem2lem1  14660  lcmfunsnlem2lem2  14661  prmind2  14684  ncoprmgcdne1b  14704  coprmproddvdslem  14728  pceq0  14869  prmreclem6  14914  0ram  15027  ram0  15029  cshwsdisj  15118  cshwsiun  15119  ressbas2  15229  ressinbas  15234  ressval3d  15235  mrcuni  15576  mreexexlem4d  15602  catpropd  15663  initoid  15949  termoid  15950  initoeu2lem0  15957  arwhoma  15989  joinfval  16296  meetfval  16310  clatlem  16406  lubun  16418  psssdm  16511  ismgmn0  16539  plusfeq  16544  isnsgrp  16580  isnmnd  16589  grpissubg  16886  idrespermg  17101  symgextfv  17108  fvcosymgeq  17119  pmtrprfv3  17144  pmtr3ncomlem1  17163  psgnunilem4  17187  gsummptfzsplitl  17615  gsumzoppg  17626  gsum2dlem1  17651  gsum2dlem2  17652  gsum2d  17653  srg1zr  17811  staffn  18126  scafeq  18160  lbsexg  18436  lidldvgen  18528  ply1bascl2  18846  cply1mul  18936  lply1binom  18949  prmirred  19115  zlmassa  19144  frgpcyg  19193  ipfeq  19266  dsmmbas2  19349  frlmbas3  19383  mamufacex  19463  matsubgcell  19508  matinvgcell  19509  matvscacell  19510  mpt2matmul  19520  matepmcl  19536  matepm2cl  19537  mat1dimbas  19546  scmatscm  19587  smatvscl  19598  marrepcl  19638  marepvcl  19643  mulmarep1el  19646  mulmarep1gsum1  19647  mulmarep1gsum2  19648  submabas  19652  nfimdetndef  19663  mdetfval1  19664  m1detdiag  19671  mdetdiag  19673  mdetunilem7  19692  mdetunilem9  19694  m2detleib  19705  gsummatr01lem3  19731  smadiadetlem4  19743  slesolinv  19754  slesolinvbi  19755  slesolex  19756  cramerimplem2  19758  pmatcoe1fsupp  19774  mat2pmatbas  19799  mat2pmatmul  19804  mat2pmatlin  19808  m2cpminvid2lem  19827  decpmatmul  19845  monmatcollpw  19852  pmatcollpw3fi  19858  pm2mpf1  19872  pm2mpghm  19889  fvmptnn04ifb  19924  cayhamlem1  19939  isbasis3g  20013  isopn2  20096  ntrval2  20115  toponmre  20158  innei  20190  restcld  20237  restcldi  20238  neitr  20245  discmp  20462  cmpsublem  20463  cmpsub  20464  2ndcctbss  20519  ssref  20576  lfinun  20589  dissnref  20592  ptcnp  20686  imasnopn  20754  imasncld  20755  imasncls  20756  kqf  20811  fbun  20904  opnfbas  20906  supfil  20959  ufprim  20973  acufl  20981  filufint  20984  ufldom  21026  hausflf2  21062  alexsubALTlem4  21114  cnextfval  21126  cnextfun  21128  cnextfres1  21132  trust  21293  utoptop  21298  ustuqtop1  21305  metustid  21618  metustfbas  21621  cfilucfil  21623  metustbl  21630  restmetu  21634  zlmclm  22175  cphassr  22238  ovolun  22501  volun  22547  vitalilem2  22616  dvmptfsum  22976  rolle  22991  ulmcaulem  23398  logfac  23599  logno1  23630  logreclem  23748  cxplogb  23772  leibpilem1  23915  prmorcht  24154  pclogsum  24192  2sqlem10  24351  chto1lb  24365  tgldimor  24595  axcontlem7  25049  usgraop  25126  ausisusgra  25131  usgra2edg1  25159  usgrarnedg  25160  usgraedg4  25163  usgra1v  25166  usgraidx2vlem2  25168  usgraidx2v  25169  usgrares1  25187  nbgrassvwo  25214  nbgrassvwo2  25215  nb3graprlem2  25229  nb3grapr  25230  nb3grapr2  25231  nb3gra2nb  25232  cusgra3v  25241  cusgrafilem2  25257  usgrasscusgra  25260  uvtxnbgra  25270  uvtxnb  25274  2trllemH  25331  2trllemE  25332  constr1trl  25367  usgra2adedgwlkonALT  25393  usgra2wlkspthlem2  25397  fargshiftfo  25415  wwlknndef  25514  wwlkextproplem3  25520  clwlkswlks  25535  clwwlknndef  25550  clwlkisclwwlklem2a4  25561  clwlkisclwwlklem1  25564  clwwlkf  25571  clwwlkvbij  25578  wwlkext2clwwlk  25580  clwwnisshclwwn  25586  erclwwlkref  25590  erclwwlknref  25602  erclwwlknsym  25603  erclwwlkntr  25604  hashecclwwlkn1  25611  usghashecclwwlk  25612  clwlkfoclwwlk  25622  el2wlkonot  25646  el2spthonot  25647  el2wlkonotot0  25649  vdgrnn0pnf  25686  clwlknclwlkdifs  25737  eupatrl  25745  frgra3v  25779  3vfriswmgra  25782  1to3vfriswmgra  25784  1to3vfriendship  25785  2pthfrgra  25788  4cycl2v2nb  25793  n4cyclfrgra  25795  frgranbnb  25797  frgrancvvdeqlem4  25810  frgrawopreg  25826  frg2woteqm  25836  usg2spot2nb  25842  numclwwlkovf2ex  25863  numclwwlk3lem  25885  grpoidinvlem3  25983  nmlno0lem  26483  blocni  26495  pythi  26540  normpythi  26844  shmodsi  27091  omlsilem  27104  pjchi  27134  chlubii  27174  osumi  27344  nmlnop0iALT  27697  cnlnssadj  27782  nmopcoi  27797  mdbr3  27999  mdbr4  28000  ssmd1  28013  dmdsl3  28017  mdslmd1lem2  28028  mdslmd4i  28035  mdexchi  28037  atssma  28080  atoml2i  28085  chirredlem3  28094  mdsymlem1  28105  mdsymlem3  28107  dmdbr6ati  28125  dmdbr7ati  28126  cdjreui  28134  cdj3lem2b  28139  addltmulALT  28148  ssrmo  28179  difuncomp  28215  iundifdif  28227  imadifxp  28261  fresf1o  28280  fimacnvinrn2  28285  sspreima  28295  acunirnmpt  28310  acunirnmpt2  28311  aciunf1lem  28313  aciunf1  28314  disjdsct  28332  1stpreimas  28335  resf1o  28364  xrge0addge  28386  xlt2addrd  28387  xrge0infssOLD  28390  f1ocnt  28425  ressmulgnn0  28495  xrge0nre  28502  gsummpt2co  28592  gsummpt2d  28593  kerunit  28635  pmtrprfv2  28660  psgnfzto1stlem  28662  fzto1st  28665  psgnfzto1st  28667  submat1n  28680  submatres  28681  lmat22lem  28692  locfinreflem  28716  ldlfcntref  28730  pstmfval  28748  mndpluscn  28781  rge0scvg  28804  pnfneige0  28806  pl1cn  28810  nexple  28880  indval2  28885  gsumesum  28929  esumcst  28933  esumrnmpt2  28938  esumcvgsum  28958  esumgect  28960  esumcvgre  28961  esum2d  28963  esumiun  28964  pwsiga  29001  insiga  29008  elsigagen2  29019  inelpisys  29025  sigapisys  29026  unelldsys  29029  ldsysgenld  29031  measxun2  29081  volmeas  29103  ddemeas  29108  aean  29116  mbfmfun  29125  mbfmbfm  29129  1stmbfm  29131  2ndmbfm  29132  omsfval  29167  omsfvalOLD  29171  oms0  29174  omssubadd  29177  oms0OLD  29178  omssubaddOLD  29181  carsgclctunlem1  29198  sibfof  29222  eulerpartlemt  29253  eulerpartlemmf  29257  eulerpartlemgs2  29262  probun  29301  dstfrvclim1  29359  coinfliprv  29364  ballotlem2  29370  ballotlemfp1  29373  ballotlemic  29388  ballotlem1c  29389  ballotlemicOLD  29426  ballotlem1cOLD  29427  plymulx0  29485  signsvtn0  29508  signstres  29513  bnj529  29600  bnj927  29629  bnj1379  29691  bnj1424  29699  bnj1436  29700  bnj1476  29707  bnj607  29776  bnj908  29791  bnj1097  29839  bnj1118  29842  bnj1128  29848  bnj1145  29851  bnj1154  29857  bnj1174  29861  bnj1189  29867  bnj1204  29870  bnj1388  29891  bnj1417  29899  cvmliftlem10  30066  mrsub0  30203  mrsubccat  30205  mrsubcn  30206  ghomgrpilem2  30353  bcprod  30423  bccolsum  30424  faclim  30431  dfon2lem3  30480  dfon2lem7  30484  dfon2lem8  30485  rdgprc0  30489  frrlem4  30566  frrlem5  30567  fvsingle  30736  unisnif  30741  funpartlem  30758  hfun  30994  trer  31021  clsun  31033  opnregcld  31035  cldregopn  31036  fnessref  31062  df3nandALT1  31106  lukshef-ax2  31124  nandsym1  31131  sylancl2  31208  bj-gl4  31224  bj-babygodel  31232  bj-babylob  31233  bj-alrimhi  31258  bj-ssbft  31300  bj-ssbequ2  31301  bj-ssbid2ALT  31304  bj-nfext  31351  bj-ax9  31543  bj-snsetex  31602  bj-1upln0  31648  bj-inftyexpidisj  31697  bj-elccinfty  31701  finixpnum  31975  fin2so  31977  poimirlem9  31994  poimirlem13  31998  poimirlem14  31999  poimirlem25  32010  poimirlem26  32011  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  mbfresfi  32032  ftc1cnnc  32061  ftc1anclem6  32067  dvasin  32073  fnopabco  32094  frinfm  32107  nninfnub  32125  caushft  32135  bndss  32163  ispridl2  32316  notornotel1  32376  tsbi2  32421  abeq12  32444  rabeq12f  32445  axc11n-16  32554  lkr0f  32705  glbconN  32987  paddssat  33424  pclunN  33508  2polssN  33525  paddunN  33537  poldmj1N  33538  ltrnnid  33746  dibglbN  34779  istopclsd  35587  pellex  35724  monotoddzzfi  35835  jm2.23  35896  expdioph  35923  dford3lem1  35926  wopprc  35930  kelac1  35966  dfac21  35969  lsmfgcl  35977  pwssplit4  35992  isnumbasgrp  36011  dgraalem  36052  dgraalemOLD  36053  ifpbi1  36166  rp-fakeanorass  36202  rp-isfinite5  36207  superficl  36216  ssuncl  36219  sssymdifcl  36221  relintab  36234  cnvssb  36237  cotrintab  36266  clcnvlem  36275  cnvtrrel  36307  brfvrcld2  36329  relexpxpmin  36354  relexpaddss  36355  brtrclfv2  36364  unhe1  36426  frege55lem1b  36536  frege58bid  36543  frege92  36596  imadisjlnd  36644  bcc0  36733  pm10.12  36751  pm11.61  36787  sbiota1  36829  bi1imp  36881  bi2imp  36882  bi3impb  36883  bi3impa  36884  bi13impib  36886  bi123impib  36887  bi13impia  36888  bi123impia  36889  bi13imp23  36892  bi13imp2  36893  bi12imp3  36894  dfvd1imp  36988  dfvd2imp  37025  e1bi  37051  e2bi  37054  e3bi  37165  3ornot23VD  37283  3impexpbicomVD  37293  3impexpbicomiVD  37294  tratrbVD  37298  ssralv2VD  37303  equncomiVD  37306  truniALTVD  37315  ee33VD  37316  csbingVD  37321  onfrALTlem3VD  37324  onfrALTlem2VD  37326  onfrALTlem1VD  37327  onfrALTVD  37328  csbsngVD  37330  csbxpgVD  37331  csbrngVD  37333  csbunigVD  37335  csbfv12gALTVD  37336  relopabVD  37338  2uasbanhVD  37348  vk15.4jVD  37351  unisnALT  37363  chordthmALT  37370  iunconlem2  37372  fnchoice  37390  elunnel2  37400  pwssfi  37419  uzwo4  37430  inabs3  37434  suprnmpt  37477  wessf1ornlem  37497  disjrnmpt2  37501  founiiun0  37503  disjf1o  37504  fompt  37505  disjinfi  37506  fvixp2  37516  choicefi  37519  fzisoeu  37556  upbdrech  37561  ssfiunibd  37565  iuneqfzuzlem  37595  iuneqfzuz  37596  xrge0ge0  37608  xrssre  37609  infrpge  37612  eliocre  37647  lbioc  37652  ioonct  37677  fsumiunss  37692  fmuldfeq  37699  infrglbOLD  37707  mccl  37716  climsuselem1  37724  climsuse  37725  ellimcabssub0  37735  islptre  37737  lptioo2  37749  lptioo1  37750  islpcn  37757  icccncfext  37803  cncfiooicclem1  37809  cncfiooicc  37810  cncfioobdlem  37812  dvbdfbdioo  37840  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvnprodlem1  37859  dvnprodlem2  37860  dvnprodlem3  37861  volioc  37887  itgioocnicc  37892  stoweidlem28  37926  stoweidlem52  37951  stoweidlem57  37956  wallispilem3  37967  wallispilem4  37968  wallispi  37970  wallispi2lem1  37971  wallispi2lem2  37972  wallispi2  37973  stirlinglem7  37980  stirlinglem10  37983  stirlinglem12  37985  fourierdlem12  38019  fourierdlem20  38027  fourierdlem25  38032  fourierdlem33  38041  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem48  38056  fourierdlem50  38058  fourierdlem52  38060  fourierdlem57  38065  fourierdlem58  38066  fourierdlem59  38067  fourierdlem65  38073  fourierdlem68  38076  fourierdlem70  38078  fourierdlem71  38079  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem80  38088  fourierdlem93  38101  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  fourierswlem  38132  fouriersw  38133  etransclem26  38163  etransclem37  38174  qndenserrnbllem  38201  saluncl  38216  intsaluni  38226  intsal  38227  salgencl  38229  salexct  38231  sssalgen  38232  salgenuni  38234  issalgend  38235  dfsalgen2  38238  salgencntex  38240  sge00  38256  sge0sn  38259  sge0cl  38261  sge0f1o  38262  sge0less  38272  sge0rnbnd  38273  sge0pnffigt  38276  sge0lefi  38278  sge0ltfirp  38280  sge0resplit  38286  sge0split  38289  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0fodjrnlem  38296  sge0iunmpt  38298  sge0isum  38307  sge0xp  38309  sge0xaddlem2  38314  iundjiun  38336  meadjun  38338  meassle  38339  meadjiunlem  38341  ismeannd  38343  meaiunlelem  38344  psmeasure  38347  carageneld  38361  caragenunidm  38367  omeunle  38375  omeiunltfirp  38378  caratheodorylem1  38385  caratheodory  38387  icoresmbl  38403  volicorescl  38413  ovncvrrp  38424  ovnsubaddlem2  38431  hoidmv1lelem1  38451  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem5  38459  hoidmvle  38460  ovnhoilem2  38462  hspdifhsp  38476  hoiqssbllem2  38483  hoiqssbllem3  38484  hspmbllem2  38487  opnvonmbllem2  38493  aifftbifffaibif  38547  aifftbifffaibifff  38548  abciffcbatnabciffncba  38555  abciffcbatnabciffncbai  38556  nabctnabc  38557  confun4  38568  confun5  38569  plcofph  38570  pldofph  38571  plvcofph  38572  plvcofphax  38573  plvofpos  38574  dandysum2p2e4  38624  2reu4a  38648  ndmaovrcl  38744  iccpartiun  38786  iccpartdisj  38789  dfodd5  38827  stgoldbwt  38915  nnsum3primesle9  38927  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  nnsum4primeseven  38933  pfxccat3  39007  pfxccatpfx1  39008  elpwdifsn  39030  pr1eqbg  39031  propeqop  39039  edgupgr  39273  ausgrusgrb  39300  ausgrumgri  39302  uspgredg2vlem  39350  uspgredg2v  39351  usgredg2vlem2  39353  usgredg2v  39354  ushgredgedga  39356  ushgredgedgaloop  39358  griedg0ssusgr  39387  umgrres1lem  39427  upgrres1  39430  usgr1v0e  39442  dfnbgr3  39458  nbgrnvtx0  39459  nbgrel  39460  nbuhgr  39461  nbuhgr2vtx1edgb  39470  nbgrssvwo2  39483  edgnbusgreu  39491  nbusgrf1o0  39493  nb3grprlem2  39505  nb3grpr2  39507  nb3gr2nb  39508  cusgredg  39542  cplgr2vpr  39550  cplgr3v  39552  umgr2v2evtxel  39609  usgrvd0nedg  39620  1wlk1walk  39697  spthdep  39766  21wlkdlem6  39880  umgr2wlkon  39899  uhgr3cyclex  39923  umgr3cyclex  39924  usgra2pthlem1  39940  usgra2pth  39941  usgvincvad  39989  usgvincvadALT  39992  usg2edgneu  39997  usgedgvadf1lem2  39999  usgedgvadf1  40000  usgedgvadf1ALTlem2  40002  usgedgvadf1ALT  40003  usgo0s0  40020  usgo0s0ALT  40021  usgo1s0ALT  40022  usgrafisbaseALT  40025  usgrafisbaseALT2  40026  usgo1s0  40027  usgfis  40031  usgfisALT  40035  lmod0rng  40141  lidldomnnring  40203  fdmdifeqresdif  40396  altgsumbcALT  40407  ply1sclrmsm  40448  lcoop  40477  lincfsuppcl  40479  linccl  40480  lincvalsng  40482  lincvalpr  40484  lincvalsc0  40487  linc0scn0  40489  lincdifsn  40490  linc1  40491  lincsum  40495  lincscm  40496  lindslinindsimp2lem5  40528  snlindsntor  40537  lincresunit3lem2  40546  ldepsnlinclem1  40571  ldepsnlinclem2  40572  difmodm1lt  40598  nn0sumshdiglemB  40704
  Copyright terms: Public domain W3C validator