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

Theorem mpdan 679
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 671 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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  df-an 377
This theorem is referenced by:  mpan2  682  mpjaodan  800  mpd3an3  1374  eueq2  3223  csbiegf  3398  difsnb  4126  reusv3i  4623  fvtresfn  5972  fvmpt3  5974  ffvelrnd  6045  fnressn  6099  fsnex  6205  f1oiso2  6267  riota5f  6300  onsucuni  6681  wfrlem5  7065  seqomlem2  7193  oaordi  7272  nnaordi  7344  qsdisj  7465  dom2lem  7634  canth2g  7751  limenpsi  7772  php4  7784  onfin  7788  sucxpdom  7806  xpfi  7867  dmfi  7879  pwfilem  7893  pwfi  7894  fiin  7961  supiso  8016  ordiso2  8055  wdom2d  8120  infeq5  8167  cantnfp1lem3  8210  cantnflem1d  8218  rankwflemb  8289  onenon  8408  cardonle  8416  sdomsdomcardi  8430  acni  8501  cardaleph  8545  cdaen  8628  cdainf  8647  infcda1  8648  pwsdompw  8659  infdif  8664  cfval  8702  fin34  8845  fin1a2lem1  8855  fin1a2  8870  ttukeylem6  8969  sdomsdomcard  9010  canth3  9011  fpwwe2  9093  canthwelem  9100  gchcda1  9106  pwfseqlem4  9112  gchcdaidm  9118  gchxpidm  9119  tskwe2  9223  rankcf  9227  tskuni  9233  gruxp  9257  dmrecnq  9418  lterpq  9420  archnq  9430  reclem3pr  9499  reclem4pr  9500  0idsr  9546  lep1  10471  ledivp1  10535  negfi  10581  supaddc  10601  supmul1  10603  suprzcl  11043  uz11  11209  zmin  11288  zbtwnre  11290  rpnnen1lem4  11321  rpnnen1lem5  11322  xnegid  11557  xrsupss  11622  xrinfmss  11623  supxrre  11641  infxrre  11650  infmxrreOLD  11654  eluzfz2  11835  fzsuc  11871  fzsuc2  11881  fzp1disj  11882  fzneuz  11903  fllep1  12068  fraclt1  12069  fracle1  12070  fracge0  12071  flhalf  12093  ceige  12103  ceim1l  12105  fldiv  12118  modval  12129  suppssfz  12237  seqeq1  12247  expubnd  12364  iexpcyc  12410  faclbnd4lem3  12511  faclbnd4lem4  12512  swrdid  12820  swrdccat3blem  12887  cshwn  12935  trclexlem  13106  shftfval  13181  shftcan1  13194  reval  13217  cjmulrcl  13255  addcj  13259  absval  13349  absneg  13388  abscj  13390  sqabsadd  13393  sqabssub  13394  leabs  13410  sqreulem  13470  lo1res  13671  o1of2  13724  o1rlimmul  13730  sumrb  13827  flo1  13960  trirecip  13969  prodrblem2  14033  efcan  14198  efi4p  14239  resin4p  14240  recos4p  14241  sincossq  14278  ruclem10  14339  iddvds  14364  1dvds  14365  2ebits  14469  lcmftp  14657  1idssfct  14678  exprmfct  14696  coprmgcdb  14702  eulerthlem2  14778  odzphi  14789  odzphiOLD  14795  pcprendvds  14838  pcmpt  14885  vdwlem8  14986  0ram2  15027  prmgaplem7  15075  pwsvscaval  15441  issect2  15707  2initoinv  15953  initoeu1  15954  initoeu2lem1  15957  initoeu2  15959  2termoinv  15960  termoeu1  15961  homarel  15979  joinfval  16295  meetfval  16309  latjcom  16353  latmcom  16369  sgrp2nmndlem5  16711  grprcan  16747  isgrpid2  16750  grpinvid  16765  mulgnn0z  16826  0subg  16890  qus0  16923  ghmker  16956  symginv  17091  pmtrfrn  17147  odmulg2  17254  slwpgp  17313  pj1eq  17398  efgtf  17420  frgpinv  17462  frgpup2  17474  mulgnn0di  17514  cnaddablx  17554  cnaddabl  17555  zaddablx  17556  dprdfadd  17701  dpjidcl  17739  dpjlid  17742  pgpfac1lem3  17758  srgen1zr  17811  ringlz  17865  ringrz  17866  1unit  17934  unitgrpid  17945  1rinv  17955  irredn0  17979  irredneg  17986  isdrng2  18033  abv0  18107  abv1z  18108  abvneg  18110  lsssn0  18219  lspsn0  18279  lsp0  18280  lmhmvsca  18316  lmhmrnlss  18321  lmhmkerlss  18322  lsppratlem5  18422  rsp1  18496  ringen1zr  18549  rlmassa  18598  asclpropd  18618  snifpsrbag  18638  psrvscaval  18664  psrdi  18678  psrdir  18679  mplsubglem  18706  mplvscaval  18720  coe1sclmulfv  18924  ply1idvr1  18934  evl1var  18972  cnfldneg  19042  zringcyg  19108  chrid  19146  chrrhm  19150  ip0r  19252  ocvlss  19283  ocv1  19290  mamuvs1  19478  mamuvs2  19479  matecl  19498  matvscacell  19509  mat0scmat  19611  submaval0  19653  mdetrsca  19676  maduval  19711  minmar1val0  19720  pmatcollpw3fi1lem2  19859  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  chcoeffeqlem  19957  cayleyhamilton0  19961  cayleyhamiltonALT  19963  cctop  20069  cldval  20086  ntrfval  20087  clsfval  20088  cmclsopn  20125  opncldf3  20150  neifval  20163  lpfval  20202  cnrmnrm  20425  islocfin  20580  tx1cn  20672  tx2cn  20673  idqtop  20769  kqtopon  20790  kqid  20791  kqcld  20798  hmphen2  20862  filssufil  20975  ufileu  20982  alexsublem  21107  symgtgp  21164  ustuqtop4  21307  ustuqtop5  21308  cstucnd  21347  metustexhalf  21619  nm0  21688  rlmnlm  21739  nmolb  21770  nmolbOLD  21789  metdseq0  21919  metdseq0OLD  21934  iocopnst  22016  pi1xfrval  22133  clmvneg1  22170  ipcau2  22256  tchcphlem1  22257  tchcphlem2  22258  cmetcaulem  22306  ovolicc2lem3  22520  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  mbfmulc2lem  22651  i1fpos  22712  mbfi1fseqlem3  22723  mbfi1fseqlem4  22724  itg2ge0  22741  dvres2  22915  dvaddbr  22940  dvmulbr  22941  dvcobr  22948  dvfsumlem4  23029  ftc1a  23037  ftc1lem6  23041  uc1pmon1p  23150  ig1pval2  23173  ig1pval2OLD  23179  dgradd2  23270  dgrcolem2  23276  plydivlem4  23297  plydiveu  23299  elqaalem3  23322  elqaalem3OLD  23325  qaa  23327  ulmdvlem1  23403  abelthlem6  23439  abelthlem7  23441  eflogeq  23599  jensenlem2  23961  harmonicbnd4  23984  sgmnncl  24122  dchrptlem2  24241  1lgs  24313  lgs1  24314  dchrisumlem2  24376  dchrisum0lem2a  24403  selberg2lem  24436  pntrsumo1  24451  pntrsumbnd  24452  pntpbnd1  24472  pntlemr  24488  pntlemj  24489  padicabvf  24517  istrkg3ld  24557  tglineeltr  24724  cusgraexilem2  25243  cusgraexi  25244  cusgrasizeinds  25252  wwlksubclwwlk  25580  erclwwlkref  25589  erclwwlknref  25601  eupacl  25745  eupapf  25748  eupaseg  25749  frgrancvvdeqlemC  25815  frghash2spot  25839  isgrpoi  25974  grpoinvfval  26000  grpoinvid  26008  grpodivfval  26018  gxfval  26033  gxid  26049  issubgo  26079  cnaddablo  26126  ghomidOLD  26141  rngolz  26177  rngorz  26178  rngosn6  26204  vcz  26237  vcoprne  26246  nvz0  26345  sspz  26422  lno0  26445  nmobndi  26464  ipasslem2  26521  shunssi  27069  ococin  27109  ssjo  27148  pjocini  27399  nlfnval  27582  lncnopbd  27738  riesz3i  27763  cnlnadjlem7  27774  pjclem4  27900  pj3si  27908  hstoc  27923  hstnmoc  27924  hstoh  27933  hst0  27934  mdsl2i  28023  chirredlem3  28093  chirredlem4  28094  dmdbr5ati  28123  rexunirn  28175  fcnvgreu  28323  infxrge0glb  28396  infxrge0glbOLD  28397  2sqcoprm  28456  omndmul2  28523  omndmul  28525  isarchi3  28552  orng0le1  28623  esumcvg  28955  esumcvgre  28960  sigaval  28980  unelldsys  29028  fiunelros  29044  measval  29068  pmeasmono  29205  eulerpartlemgvv  29257  probfinmeasb  29310  ballotlemfc0  29373  ballotlemfcc  29374  ballotlemsi  29395  ballotlemfrci  29408  ballotlemsiOLD  29433  ballotlemfrciOLD  29446  sgnneg  29459  signlem0  29524  bnj1006  29818  bnj1110  29839  bnj1253  29874  bnj1280  29877  bnj1463  29912  bnj1312  29915  erdszelem7  29968  erdszelem8  29969  cvmliftlem10  30065  cvmliftlem13  30067  cvmlift2lem9  30082  cvmlift3lem6  30095  cvmlift3lem7  30096  cvmlift3lem9  30098  ghomgrpilem2  30352  dfrdg2  30490  dftrpred3g  30522  frrlem5  30566  bdayval  30583  cldregopn  31035  tailfval  31076  filnetlem3  31084  filnetlem4  31085  ontopbas  31136  f1omptsnlem  31782  icoreunrn  31806  relowlpssretop  31811  wl-sbal2  31938  poimirlem1  31985  poimirlem2  31986  poimirlem4  31988  poimirlem6  31990  poimirlem7  31991  poimirlem11  31995  poimirlem12  31996  poimirlem17  32001  poimirlem20  32004  poimirlem22  32006  poimirlem23  32007  poimirlem28  32012  poimir  32017  ismblfin  32025  cnambfre  32033  bddiblnc  32056  ftc1cnnc  32060  dvasin  32072  ismtyres  32184  heiborlem8  32194  rngonegmn1l  32232  rngonegmn1r  32233  rngoneglmul  32234  rngonegrmul  32235  idlnegcl  32299  0idl  32302  0rngo  32304  keridl  32309  smprngopr  32329  lshpne0  32596  lkrval  32698  ldualvaddval  32741  ldualvsval  32748  opoc1  32812  pmap0  33374  pmap1N  33376  pexmidALTN  33587  cdleme31fv  34001  cdlemg27b  34307  erngdvlem4  34602  erng0g  34605  erngdvlem4-rN  34610  dvalveclem  34637  dvh0g  34723  dih0cnv  34895  dih1rn  34899  dih1cnv  34900  doch0  34970  doch1  34971  lcfl7lem  35111  mapdheq  35340  hdmap1eq  35414  hdmapval2lem  35446  hgmapvvlem3  35540  mzpval  35618  mzpindd  35632  pellex  35723  2nn0ind  35837  jm2.26lem3  35900  pw2f1o2val  35938  wepwsolem  35944  fnwe2lem3  35954  lnmfg  35984  dgrsub2  36038  mpaaeu  36060  flcidc  36084  rtrclexlem  36267  cnvrcl0  36276  suprleubrd  36653  suprlubrd  36657  imo72b2  36662  dvconstbi  36726  bcc0  36732  binomcxplemnotnn0  36748  nnfoctb  37420  sumnnodd  37747  icccncfext  37802  itgsin0pilem1  37863  stoweidlem22  37919  stoweidlem32  37930  stoweidlem35  37933  stoweidlem36  37934  stoweidlem37  37935  stoweidlem43  37941  stoweidlem50  37948  wallispilem5  37968  stirlinglem2  37974  stirlinglem3  37975  stirlinglem4  37976  stirlinglem8  37980  stirlinglem11  37983  stirlinglem12  37984  stirlinglem14  37986  stirlinglem15  37987  fourierdlem11  38017  fourierdlem20  38026  fourierdlem21  38027  fourierdlem41  38048  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem48  38055  fourierdlem49  38056  fourierdlem64  38071  fourierdlem71  38078  fourierdlem79  38086  fourierdlem90  38097  fourierdlem91  38098  fourierswlem  38131  etransclem17  38153  etransclem38  38174  bgoldbtbndlem2  38938  bgoldbtbndlem3  38939  bgoldbtbnd  38941  pfxid  38972  pfx2  38992  structiedg0val  39169  incistruhgr  39217  uhgredgiedgb  39264  uhgriedg0edg0  39266  subgrprop3  39397  subgruhgredgd  39405  usgrexi  39555  cusgrexi  39556  cusgrsizeinds  39562  vtxduhgr0e  39586  vtxdgfusgrf  39600  ewlkprop  39669  2pthnloop  39763  1trld  39856  1pthd  39857  2trld  39886  2spthd  39889  umgr2wlkon  39898  3spthd  39916  3cycld  39918  usgrauvtxvd  39944  vdcusgra  39945  usgedgvadf1lem2  39998  usgedgvadf1ALTlem2  40001  isclintop  40115  clintopcllaw  40119  nzrneg1ne0  40141  rnglz  40156  c0snmgmhm  40186  zrrnghm  40189  lidldomn1  40193  uzlidlring  40201  2zrngnmlid  40221  cznrng  40229  zrinitorngc  40274  zrtermorngc  40275  zrtermoringc  40344  coe1id  40448  blenre  40657  blennn  40658
  Copyright terms: Public domain W3C validator