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

Theorem mpdan 668
Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
mpdan.1  |-  ( ph  ->  ps )
mpdan.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpdan  |-  ( ph  ->  ch )

Proof of Theorem mpdan
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  mpan2  671  mpjaodan  784  mpd3an3  1315  eueq2  3128  csbiegf  3307  difsnb  4010  reusv3i  4494  fvtresfn  5770  fvmpt3  5772  ffvelrnd  5839  fnressn  5889  f1oiso2  6038  riota5f  6072  onsucuni  6434  seqomlem2  6898  oaordi  6977  nnaordi  7049  qsdisj  7169  dom2lem  7341  canth2g  7457  limenpsi  7478  php4  7490  onfin  7493  sucxpdom  7514  xpfi  7575  dmfi  7586  pwfilem  7597  pwfi  7598  fiin  7664  supiso  7714  ordiso2  7721  wemaplem2  7753  wdom2d  7787  infeq5  7835  cantnfp1lem3  7880  cantnflem1d  7888  cantnfp1lem3OLD  7906  cantnflem1dOLD  7911  r1val1  7985  rankwflemb  7992  onenon  8111  cardonle  8119  sdomsdomcardi  8133  acni  8207  cardaleph  8251  cdaen  8334  cdainf  8353  infcda1  8354  pwsdompw  8365  infdif  8370  cfval  8408  fin34  8551  fin1a2lem1  8561  fin1a2  8576  ttukeylem6  8675  sdomsdomcard  8716  canth3  8717  fpwwe2  8802  canthwelem  8809  gchcda1  8815  pwfseqlem4  8821  gchcdaidm  8827  gchxpidm  8828  tskwe2  8932  rankcf  8936  tskuni  8942  gruxp  8966  dmrecnq  9129  lterpq  9131  archnq  9141  reclem3pr  9210  reclem4pr  9211  0idsr  9256  lep1  10160  ledivp1  10226  supmul1  10287  suprzcl  10713  uz11  10875  zmin  10941  zbtwnre  10943  rpnnen1lem4  10974  rpnnen1lem5  10975  xnegid  11198  xleadd1a  11208  xlt2add  11215  xmullem  11219  xmulgt0  11238  xmulasslem3  11241  xlemul1a  11243  xadddilem  11249  xadddi  11250  xadddi2  11252  xrsupss  11263  xrinfmss  11264  supxrre  11282  infmxrre  11290  eluzfz2  11451  fzsuc  11494  fzsuc2  11506  fzp1disj  11507  fzneuz  11533  fllep1  11643  fraclt1  11644  fracle1  11645  fracge0  11646  flhalf  11666  ceige  11676  ceim1l  11678  fldiv  11691  modval  11702  seqeq1  11801  expubnd  11916  iexpcyc  11962  faclbnd4lem3  12063  faclbnd4lem4  12064  swrdccat3blem  12378  cshwn  12426  shftfval  12551  shftcan1  12564  reval  12587  cjmulrcl  12625  addcj  12629  absval  12719  absneg  12758  abscj  12760  sqabsadd  12763  sqabssub  12764  leabs  12780  sqreulem  12839  lo1res  13029  o1of2  13082  o1rlimmul  13088  sumrb  13182  flo1  13309  trirecip  13317  efcan  13372  efi4p  13413  resin4p  13414  recos4p  13415  sincossq  13452  ruclem10  13513  iddvds  13538  1dvds  13539  2ebits  13635  1idssfct  13761  exprmfct  13788  eulerthlem2  13849  odzphi  13860  pcprendvds  13899  pcmpt  13946  vdwlem8  14041  0ram2  14074  pwsvscaval  14425  issect2  14685  homarel  14896  joinfval  15163  meetfval  15177  latjcom  15221  latmcom  15237  grprcan  15562  isgrpid2  15565  grpinvid  15580  mulgnn0z  15638  0subg  15697  divs0  15730  ghmker  15763  symginv  15898  symgfixfvh  15932  pmtrfrn  15955  odmulg2  16047  slwpgp  16103  pj1eq  16188  efgtf  16210  frgpinv  16252  frgpup2  16264  mulgnn0di  16304  cnaddablx  16339  cnaddabl  16340  zaddablx  16341  dprdfadd  16500  dprdfaddOLD  16507  dpjidcl  16547  dpjlid  16550  dpjidclOLD  16554  pgpfac1lem3  16568  rnglz  16671  rngrz  16672  1unit  16740  unitgrpid  16751  1rinv  16761  irredn0  16785  irredneg  16792  isdrng2  16822  abv0  16896  abv1z  16897  abvneg  16899  lsssn0  17009  lspsn0  17069  lsp0  17070  lmhmvsca  17106  lmhmrnlss  17111  lmhmkerlss  17112  lsppratlem5  17212  rsp1  17286  rlmassa  17377  asclpropd  17396  snifpsrbag  17413  psrvscaval  17443  psrdi  17459  psrdir  17460  mplsubglem  17490  mplsubglemOLD  17492  mplvscaval  17507  coe1sclmulfv  17716  evl1var  17750  cnfldneg  17822  zringcyg  17887  zcyg  17892  chrid  17938  chrrhm  17942  ip0r  18046  ocvlss  18077  ocv1  18084  mamuvs1  18289  mamuvs2  18290  matecl  18306  submaval0  18371  mdetrsca  18390  maduval  18424  minmar1val0  18433  cctop  18590  cldval  18607  ntrfval  18608  clsfval  18609  cmclsopn  18646  opncldf3  18670  neifval  18683  lpfval  18722  cnrmnrm  18945  tx1cn  19162  tx2cn  19163  idqtop  19259  kqtopon  19280  kqid  19281  kqcld  19288  hmphen2  19352  filssufil  19465  ufileu  19472  alexsublem  19596  symgtgp  19652  ustuqtop4  19799  ustuqtop5  19800  cstucnd  19839  isxmet2d  19882  metustexhalfOLD  20118  metustexhalf  20119  nm0  20198  rlmnlm  20249  nmolb  20276  metdseq0  20410  iocopnst  20492  icccvx  20502  pi1xfrval  20606  clmvneg1  20643  ipcau2  20729  tchcphlem1  20730  tchcphlem2  20731  cmetcaulem  20779  ivthicc  20922  ovolicc2lem3  20982  ovolicc2lem4  20983  mbfmulc2lem  21105  i1fpos  21164  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  itg2ge0  21193  dvres2  21367  dvaddbr  21392  dvmulbr  21393  dvcobr  21400  c1lip1  21449  dvivth  21462  dvfsumlem4  21481  ftc1a  21489  ftc1lem6  21493  uc1pmon1p  21603  ig1pval2  21625  dgradd2  21715  dgrcolem2  21721  plydivlem4  21742  plydiveu  21744  elqaalem3  21767  qaa  21769  ulmdvlem1  21845  abelthlem6  21881  abelthlem7  21883  reeff1o  21892  coseq00topi  21944  tanabsge  21948  eflogeq  22030  logcnlem3  22069  atantan  22298  atanbnd  22301  cvxcl  22358  jensenlem2  22361  harmonicbnd4  22384  sgmnncl  22465  dchrptlem2  22584  1lgs  22656  lgs1  22657  dchrisumlem2  22719  dchrisum0lem2a  22746  selberg2lem  22779  pntrsumo1  22794  pntrsumbnd  22795  pntpbnd1  22815  pntlemr  22831  pntlemj  22832  ostthlem1  22856  padicabvf  22860  tglineeltr  23017  ttgval  23089  xmstrkgc  23100  cusgraexilem2  23343  cusgraexi  23344  cusgrasizeinds  23352  eupacl  23558  eupapf  23561  eupaseg  23562  isgrpoi  23653  grpoinvfval  23679  grpoinvid  23687  grpodivfval  23697  gxfval  23712  gxid  23728  issubgo  23758  cnaddablo  23805  ghomid  23820  rngolz  23856  rngorz  23857  rngosn6  23883  vcz  23916  vcoprne  23925  nvz0  24024  sspz  24101  lno0  24124  nmobndi  24143  ipasslem2  24200  shunssi  24739  ococin  24779  ssjo  24818  pjocini  25069  nlfnval  25253  lncnopbd  25409  riesz3i  25434  cnlnadjlem7  25445  pjclem4  25571  pj3si  25579  hstoc  25594  hstnmoc  25595  hstoh  25604  hst0  25605  mdsl2i  25694  chirredlem3  25764  chirredlem4  25765  dmdbr5ati  25794  rexunirn  25843  fcnvgreu  25959  xrpxdivcld  26078  omndmul2  26143  omndmul  26145  isarchi3  26172  orng0le1  26248  esumcst  26483  esumcvg  26504  sigaval  26522  measval  26581  eulerpartlemgvv  26728  probfinmeasb  26781  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemsi  26866  ballotlemfrci  26879  signspval  26922  signlem0  26957  erdszelem7  27054  erdszelem8  27055  cvmliftlem10  27152  cvmliftlem13  27154  cvmlift2lem9  27169  cvmlift3lem6  27182  cvmlift3lem7  27183  cvmlift3lem9  27185  ghomgrpilem2  27274  prodrblem2  27413  dfrdg2  27578  dftrpred3g  27666  wfrlem5  27697  frrlem5  27741  bdayval  27758  ontopbas  28244  supaddc  28388  ismblfin  28403  cnambfre  28411  bddiblnc  28433  ftc1cnnc  28437  dvasin  28451  cldregopn  28497  islocfin  28539  tailfval  28564  filnetlem3  28572  filnetlem4  28573  ismtyres  28678  heiborlem8  28688  rngonegmn1l  28726  rngonegmn1r  28727  rngoneglmul  28728  rngonegrmul  28729  idlnegcl  28793  0idl  28796  0rngo  28798  keridl  28803  smprngopr  28823  mzpval  29039  mzpindd  29053  pellex  29147  2nn0ind  29257  jm2.26lem3  29321  pw2f1o2val  29359  wepwsolem  29365  fnwe2lem3  29376  lnmfg  29406  dgrsub2  29462  mpaaeu  29478  flcidc  29502  dvconstbi  29579  itgsin0pilem1  29761  stoweidlem22  29788  stoweidlem32  29798  stoweidlem35  29801  stoweidlem36  29802  stoweidlem37  29803  stoweidlem43  29809  stoweidlem50  29816  wallispilem5  29835  stirlinglem2  29841  stirlinglem3  29842  stirlinglem4  29843  stirlinglem8  29847  stirlinglem11  29850  stirlinglem12  29851  stirlinglem14  29853  stirlinglem15  29854  wwlksubclwwlk  30437  erclwwlkref  30454  erclwwlknref  30470  usgrauvtxvd  30501  vdcusgra  30502  frgrancvvdeqlemC  30603  frghash2spot  30627  nzrneg1ne0  30749  suppssfz  30755  ply1idvr1  30793  coe1id  30799  matvscacell  30821  bnj1006  31881  bnj1110  31902  bnj1253  31937  bnj1280  31940  bnj1463  31975  bnj1312  31978  lshpne0  32524  lkrval  32626  ldualvaddval  32669  ldualvsval  32676  opoc1  32740  pmap0  33302  pmap1N  33304  pexmidALTN  33515  cdleme31fv  33927  cdlemg27b  34233  erngdvlem4  34528  erng0g  34531  erngdvlem4-rN  34536  dvalveclem  34563  dvh0g  34649  dih0cnv  34821  dih1rn  34825  dih1cnv  34826  doch0  34896  doch1  34897  lcfl7lem  35037  mapdheq  35266  hdmap1eq  35340  hdmapval2lem  35372  hgmapvvlem3  35466
  Copyright terms: Public domain W3C validator