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  786  mpd3an3  1326  eueq2  3259  csbiegf  3444  difsnb  4157  reusv3i  4644  fvtresfn  5942  fvmpt3  5944  ffvelrnd  6017  fnressn  6068  f1oiso2  6233  riota5f  6267  onsucuni  6648  seqomlem2  7118  oaordi  7197  nnaordi  7269  qsdisj  7390  dom2lem  7557  canth2g  7673  limenpsi  7694  php4  7706  onfin  7710  sucxpdom  7731  xpfi  7793  dmfi  7805  pwfilem  7816  pwfi  7817  fiin  7884  supiso  7936  ordiso2  7943  wdom2d  8009  infeq5  8057  cantnfp1lem3  8102  cantnflem1d  8110  cantnfp1lem3OLD  8128  cantnflem1dOLD  8133  rankwflemb  8214  onenon  8333  cardonle  8341  sdomsdomcardi  8355  acni  8429  cardaleph  8473  cdaen  8556  cdainf  8575  infcda1  8576  pwsdompw  8587  infdif  8592  cfval  8630  fin34  8773  fin1a2lem1  8783  fin1a2  8798  ttukeylem6  8897  sdomsdomcard  8938  canth3  8939  fpwwe2  9024  canthwelem  9031  gchcda1  9037  pwfseqlem4  9043  gchcdaidm  9049  gchxpidm  9050  tskwe2  9154  rankcf  9158  tskuni  9164  gruxp  9188  dmrecnq  9349  lterpq  9351  archnq  9361  reclem3pr  9430  reclem4pr  9431  0idsr  9477  lep1  10387  ledivp1  10453  supmul1  10514  suprzcl  10948  uz11  11112  zmin  11187  zbtwnre  11189  rpnnen1lem4  11220  rpnnen1lem5  11221  xnegid  11444  xrsupss  11509  xrinfmss  11510  supxrre  11528  infmxrre  11536  eluzfz2  11703  fzsuc  11736  fzsuc2  11746  fzp1disj  11747  fzneuz  11768  fllep1  11917  fraclt1  11918  fracle1  11919  fracge0  11920  flhalf  11941  ceige  11951  ceim1l  11953  fldiv  11966  modval  11977  suppssfz  12079  seqeq1  12089  expubnd  12205  iexpcyc  12251  faclbnd4lem3  12352  faclbnd4lem4  12353  swrdccat3blem  12699  cshwn  12747  shftfval  12882  shftcan1  12895  reval  12918  cjmulrcl  12956  addcj  12960  absval  13050  absneg  13089  abscj  13091  sqabsadd  13094  sqabssub  13095  leabs  13111  sqreulem  13171  lo1res  13361  o1of2  13414  o1rlimmul  13420  sumrb  13514  flo1  13645  trirecip  13653  efcan  13708  efi4p  13749  resin4p  13750  recos4p  13751  sincossq  13788  ruclem10  13849  iddvds  13874  1dvds  13875  2ebits  13974  1idssfct  14100  exprmfct  14128  eulerthlem2  14189  odzphi  14200  pcprendvds  14241  pcmpt  14288  vdwlem8  14383  0ram2  14416  pwsvscaval  14769  issect2  15026  homarel  15237  joinfval  15505  meetfval  15519  latjcom  15563  latmcom  15579  sgrp2nmndlem5  15921  grprcan  15957  isgrpid2  15960  grpinvid  15975  mulgnn0z  16036  0subg  16100  qus0  16133  ghmker  16166  symginv  16301  pmtrfrn  16357  odmulg2  16451  slwpgp  16507  pj1eq  16592  efgtf  16614  frgpinv  16656  frgpup2  16668  mulgnn0di  16708  cnaddablx  16748  cnaddabl  16749  zaddablx  16750  dprdfadd  16934  dprdfaddOLD  16941  dpjidcl  16981  dpjlid  16984  dpjidclOLD  16988  pgpfac1lem3  17002  srgen1zr  17055  ringlz  17109  ringrz  17110  1unit  17181  unitgrpid  17192  1rinv  17202  irredn0  17226  irredneg  17233  isdrng2  17280  abv0  17354  abv1z  17355  abvneg  17357  lsssn0  17468  lspsn0  17528  lsp0  17529  lmhmvsca  17565  lmhmrnlss  17570  lmhmkerlss  17571  lsppratlem5  17671  rsp1  17746  ringen1zr  17799  rlmassa  17849  asclpropd  17869  snifpsrbag  17889  psrvscaval  17919  psrdi  17935  psrdir  17936  mplsubglem  17967  mplsubglemOLD  17969  mplvscaval  17984  coe1sclmulfv  18198  ply1idvr1  18208  evl1var  18246  cnfldneg  18318  zringcyg  18386  zcyg  18391  chrid  18437  chrrhm  18441  ip0r  18545  ocvlss  18576  ocv1  18583  mamuvs1  18780  mamuvs2  18781  matecl  18800  matvscacell  18811  mat0scmat  18913  submaval0  18955  mdetrsca  18978  maduval  19013  minmar1val0  19022  pmatcollpw3fi1lem2  19161  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  chcoeffeqlem  19259  cayleyhamilton0  19263  cayleyhamiltonALT  19265  cctop  19380  cldval  19397  ntrfval  19398  clsfval  19399  cmclsopn  19436  opncldf3  19460  neifval  19473  lpfval  19512  cnrmnrm  19735  islocfin  19891  tx1cn  19983  tx2cn  19984  idqtop  20080  kqtopon  20101  kqid  20102  kqcld  20109  hmphen2  20173  filssufil  20286  ufileu  20293  alexsublem  20417  symgtgp  20473  ustuqtop4  20620  ustuqtop5  20621  cstucnd  20660  metustexhalfOLD  20939  metustexhalf  20940  nm0  21019  rlmnlm  21070  nmolb  21097  metdseq0  21231  iocopnst  21313  pi1xfrval  21427  clmvneg1  21464  ipcau2  21550  tchcphlem1  21551  tchcphlem2  21552  cmetcaulem  21600  ovolicc2lem3  21803  ovolicc2lem4  21804  mbfmulc2lem  21927  i1fpos  21986  mbfi1fseqlem3  21997  mbfi1fseqlem4  21998  itg2ge0  22015  dvres2  22189  dvaddbr  22214  dvmulbr  22215  dvcobr  22222  dvfsumlem4  22303  ftc1a  22311  ftc1lem6  22315  uc1pmon1p  22425  ig1pval2  22447  dgradd2  22537  dgrcolem2  22543  plydivlem4  22564  plydiveu  22566  elqaalem3  22589  qaa  22591  ulmdvlem1  22667  abelthlem6  22703  abelthlem7  22705  eflogeq  22858  jensenlem2  23189  harmonicbnd4  23212  sgmnncl  23293  dchrptlem2  23412  1lgs  23484  lgs1  23485  dchrisumlem2  23547  dchrisum0lem2a  23574  selberg2lem  23607  pntrsumo1  23622  pntrsumbnd  23623  pntpbnd1  23643  pntlemr  23659  pntlemj  23660  padicabvf  23688  tglineeltr  23883  cusgraexilem2  24339  cusgraexi  24340  cusgrasizeinds  24348  wwlksubclwwlk  24676  erclwwlkref  24685  erclwwlknref  24697  eupacl  24841  eupapf  24844  eupaseg  24845  frgrancvvdeqlemC  24911  frghash2spot  24935  isgrpoi  25072  grpoinvfval  25098  grpoinvid  25106  grpodivfval  25116  gxfval  25131  gxid  25147  issubgo  25177  cnaddablo  25224  ghomidOLD  25239  rngolz  25275  rngorz  25276  rngosn6  25302  vcz  25335  vcoprne  25344  nvz0  25443  sspz  25520  lno0  25543  nmobndi  25562  ipasslem2  25619  shunssi  26158  ococin  26198  ssjo  26237  pjocini  26488  nlfnval  26672  lncnopbd  26828  riesz3i  26853  cnlnadjlem7  26864  pjclem4  26990  pj3si  26998  hstoc  27013  hstnmoc  27014  hstoh  27023  hst0  27024  mdsl2i  27113  chirredlem3  27183  chirredlem4  27184  dmdbr5ati  27213  rexunirn  27262  fcnvgreu  27386  2sqcoprm  27508  omndmul2  27575  omndmul  27577  isarchi3  27604  orng0le1  27675  esumcvg  27965  sigaval  27983  measval  28042  eulerpartlemgvv  28188  probfinmeasb  28241  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemsi  28326  ballotlemfrci  28339  sgnneg  28352  signlem0  28417  erdszelem7  28514  erdszelem8  28515  cvmliftlem10  28612  cvmliftlem13  28614  cvmlift2lem9  28629  cvmlift3lem6  28642  cvmlift3lem7  28643  cvmlift3lem9  28645  ghomgrpilem2  28899  prodrblem2  29038  dfrdg2  29203  dftrpred3g  29291  wfrlem5  29322  frrlem5  29366  bdayval  29383  ontopbas  29868  wl-sbal2  29989  supaddc  30016  ismblfin  30030  cnambfre  30038  bddiblnc  30060  ftc1cnnc  30064  dvasin  30078  cldregopn  30124  tailfval  30165  filnetlem3  30173  filnetlem4  30174  ismtyres  30279  heiborlem8  30289  rngonegmn1l  30327  rngonegmn1r  30328  rngoneglmul  30329  rngonegrmul  30330  idlnegcl  30394  0idl  30397  0rngo  30399  keridl  30404  smprngopr  30424  mzpval  30639  mzpindd  30653  pellex  30746  2nn0ind  30856  jm2.26lem3  30918  pw2f1o2val  30956  wepwsolem  30962  fnwe2lem3  30973  lnmfg  31003  dgrsub2  31059  mpaaeu  31075  flcidc  31099  dvconstbi  31215  sumnnodd  31544  icccncfext  31597  itgsin0pilem1  31638  stoweidlem22  31693  stoweidlem32  31703  stoweidlem35  31706  stoweidlem36  31707  stoweidlem37  31708  stoweidlem43  31714  stoweidlem50  31721  wallispilem5  31740  stirlinglem2  31746  stirlinglem3  31747  stirlinglem4  31748  stirlinglem8  31752  stirlinglem11  31755  stirlinglem12  31756  stirlinglem14  31758  stirlinglem15  31759  fourierdlem11  31789  fourierdlem20  31798  fourierdlem21  31799  fourierdlem41  31819  fourierdlem42  31820  fourierdlem48  31826  fourierdlem49  31827  fourierdlem64  31842  fourierdlem71  31849  fourierdlem79  31857  fourierdlem90  31868  fourierdlem91  31869  fourierswlem  31902  usgrauvtxvd  32196  vdcusgra  32197  usgedgvadf1lem2  32252  usgedgvadf1ALTlem2  32255  isclintop  32368  clintopcllaw  32372  lidldomn1  32437  uzlidlring  32445  2zrngnmlid  32465  cznrng  32473  nzrneg1ne0  32695  coe1id  32719  bnj1006  33750  bnj1110  33771  bnj1253  33806  bnj1280  33809  bnj1463  33844  bnj1312  33847  lshpne0  34451  lkrval  34553  ldualvaddval  34596  ldualvsval  34603  opoc1  34667  pmap0  35229  pmap1N  35231  pexmidALTN  35442  cdleme31fv  35856  cdlemg27b  36162  erngdvlem4  36457  erng0g  36460  erngdvlem4-rN  36465  dvalveclem  36492  dvh0g  36578  dih0cnv  36750  dih1rn  36754  dih1cnv  36755  doch0  36825  doch1  36826  lcfl7lem  36966  mapdheq  37195  hdmap1eq  37269  hdmapval2lem  37301  hgmapvvlem3  37395  suprleubrd  37652  suprlubrd  37656  imo72b2  37662
  Copyright terms: Public domain W3C validator