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

Theorem mpdan 649
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 19 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpan2  652  mpjaodan  761  mpd3an3  1278  eueq2  2939  csbiegf  3121  difsneq  3757  reusv3i  4541  onsucuni  4619  fvmpt3  5604  ffvelrnd  5666  fnressn  5705  f1oiso2  5849  riota5f  6329  riotasvdOLD  6348  seqomlem2  6463  oaordi  6544  nnaordi  6616  qsdisj  6736  dom2lem  6901  canth2g  7015  limenpsi  7036  php4  7048  onfin  7051  sucxpdom  7072  xpfi  7128  dmfi  7139  pwfilem  7150  pwfi  7151  fiin  7175  supiso  7223  ordiso2  7230  wemaplem2  7262  wdom2d  7294  infeq5  7338  cantnfp1lem3  7382  cantnflem1d  7390  r1val1  7458  rankwflemb  7465  onenon  7582  cardonle  7590  sdomsdomcardi  7604  acni  7672  cardaleph  7716  cdaen  7799  cdainf  7818  infcda1  7819  pwsdompw  7830  infdif  7835  cfval  7873  fin34  8016  fin1a2lem1  8026  fin1a2  8041  ttukeylem6  8141  sdomsdomcard  8182  canth3  8183  fpwwe2  8265  canthwelem  8272  gchcda1  8278  pwfseqlem4  8284  gchcdaidm  8290  gchxpidm  8291  tskwe2  8395  rankcf  8399  tskuni  8405  gruxp  8429  dmrecnq  8592  lterpq  8594  archnq  8604  reclem3pr  8673  reclem4pr  8674  0idsr  8719  lep1  9595  ledivp1  9658  supmul1  9719  suprzcl  10091  uz11  10250  zmin  10312  zbtwnre  10314  rpnnen1lem4  10345  rpnnen1lem5  10346  xnegid  10563  xleadd1a  10573  xlt2add  10580  xmullem  10584  xmulgt0  10603  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xadddi  10615  xadddi2  10617  xrsupss  10627  xrinfmss  10628  supxrre  10646  infmxrre  10654  eluzfz2  10804  fzsuc  10835  fzsuc2  10842  fzp1disj  10843  fzneuz  10863  fllep1  10933  fraclt1  10934  fracle1  10935  fracge0  10936  flhalf  10954  ceige  10956  ceim1l  10957  fldiv  10964  modval  10975  seqeq1  11049  expubnd  11162  iexpcyc  11207  faclbnd4lem3  11308  faclbnd4lem4  11309  shftfval  11565  shftcan1  11578  reval  11591  cjmulrcl  11629  addcj  11633  absval  11723  absneg  11762  abscj  11764  sqabsadd  11767  sqabssub  11768  leabs  11784  sqreulem  11843  lo1res  12033  o1of2  12086  o1rlimmul  12092  sumrb  12186  flo1  12313  trirecip  12321  efcan  12376  efi4p  12417  resin4p  12418  recos4p  12419  sincossq  12456  ruclem10  12517  iddvds  12542  1dvds  12543  2ebits  12638  1idssfct  12764  exprmfct  12789  eulerthlem2  12850  odzphi  12861  pcprendvds  12893  pcmpt  12940  vdwlem8  13035  0ram2  13068  pwsvscaval  13394  issect2  13657  homarel  13868  latjcom  14165  latlej1  14166  latlej2  14167  latmcom  14181  latmle1  14182  latmle2  14183  lubun  14227  grprcan  14515  isgrpid2  14518  grpinvid  14533  mulgnn0z  14587  0subg  14642  divs0  14675  ghmker  14708  symginv  14782  odval2  14866  odmulg2  14868  slwpgp  14924  pj1eq  15009  efgtf  15031  frgpinv  15073  frgpup2  15085  mulgnn0di  15125  cnaddablx  15158  cnaddabl  15159  zaddablx  15160  dprdfadd  15255  dpjidcl  15293  dpjlid  15296  pgpfac1lem3  15312  rnglz  15377  rngrz  15378  1unit  15440  unitgrpid  15451  1rinv  15461  irredn0  15485  irredneg  15492  isdrng2  15522  abv0  15596  abv1z  15597  abvneg  15599  lsssn0  15705  lspsn0  15765  lsp0  15766  lmhmvsca  15802  lmhmrnlss  15807  lmhmkerlss  15808  lsppratlem5  15904  rsp1  15976  rlmassa  16066  asclpropd  16085  psrvscaval  16137  psrdi  16151  psrdir  16152  mplsubglem  16179  mplvscaval  16192  coe1sclmulfv  16359  cnfldneg  16400  zcyg  16445  chrid  16481  chrrhm  16485  ip0r  16541  ocvlss  16572  ocv1  16579  cctop  16743  cldval  16760  ntrfval  16761  clsfval  16762  cmclsopn  16799  opncldf3  16823  neifval  16836  lpfval  16870  cnrmnrm  17089  tx1cn  17303  tx2cn  17304  idqtop  17397  kqtopon  17418  kqid  17419  kqcld  17426  hmphen2  17490  filssufil  17607  ufileu  17614  alexsublem  17738  symgtgp  17784  isxmet2d  17892  nm0  18148  rlmnlm  18199  nmolb  18226  metdseq0  18358  iocopnst  18438  icccvx  18448  pi1xfrval  18552  clmvneg1  18589  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  cmetcaulem  18714  ivthicc  18818  ovolicc2lem3  18878  ovolicc2lem4  18879  mbfmulc2lem  19002  i1fpos  19061  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  itg2ge0  19090  dvres2  19262  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  c1lip1  19344  dvivth  19357  dvfsumlem4  19376  ftc1a  19384  ftc1lem6  19388  evl1var  19415  uc1pmon1p  19537  ig1pval2  19559  dgradd2  19649  dgrcolem2  19655  plydivlem4  19676  plydiveu  19678  elqaalem3  19701  qaa  19703  ulmdvlem1  19777  abelthlem6  19812  abelthlem7  19814  reeff1o  19823  coseq00topi  19870  tanabsge  19874  eflogeq  19955  logcnlem3  19991  atantan  20219  atanbnd  20222  cvxcl  20279  jensenlem2  20282  harmonicbnd4  20304  sgmnncl  20385  dchrptlem2  20504  1lgs  20576  lgs1  20577  dchrisumlem2  20639  dchrisum0lem2a  20666  selberg2lem  20699  pntrsumo1  20714  pntrsumbnd  20715  pntpbnd1  20735  pntlemr  20751  pntlemj  20752  ostthlem1  20776  padicabvf  20780  isgrpoi  20865  grpoinvfval  20891  grpoinvid  20899  grpodivfval  20909  gxfval  20924  gxid  20940  issubgo  20970  cnaddablo  21017  ghomid  21032  rngolz  21068  rngorz  21069  rngosn6  21095  vcz  21126  vcoprne  21135  nvz0  21234  sspz  21311  lno0  21334  nmobndi  21353  ipasslem2  21410  shunssi  21947  ococin  21987  ssjo  22026  pjocini  22277  nlfnval  22461  adjvalval  22517  lncnopbd  22617  riesz3i  22642  cnlnadjlem7  22653  pjclem4  22779  pj3si  22787  hstoc  22802  hstnmoc  22803  hstoh  22812  hst0  22813  mdsl2i  22902  chirredlem3  22972  chirredlem4  22973  dmdbr5ati  23002  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsi  23073  ballotlemfrci  23086  xrpxdivcld  23119  rexunirn  23140  abfmpel  23219  rnlogblem  23401  esumcst  23436  esumcvg  23454  sigaval  23471  measval  23529  measiuns  23544  probfinmeasb  23632  erdszelem7  23728  erdszelem8  23729  cvmliftlem10  23825  cvmliftlem13  23827  cvmlift2lem9  23842  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  eupacl  23884  eupapf  23887  eupaseg  23888  ghomgrpilem2  23993  dfrdg2  24152  dftrpred3g  24236  wfrlem5  24260  frrlem5  24285  bdayval  24302  ontopbas  24867  sege  25252  fincmpzer  25350  mulveczer  25479  svli2  25484  mslb1  25607  sigadd  25649  valvze  25654  fnmulcv  25684  imonclem  25813  isinob  25862  carinttar2  25903  prismorcsetlem  25912  morcatset1  25915  domcatfun  25925  codcatfun  25934  idcatfun  25941  nds  26150  cldregopn  26249  islocfin  26296  tailfval  26321  filnetlem3  26329  filnetlem4  26330  ismtyres  26532  heiborlem8  26542  rngonegmn1l  26580  rngonegmn1r  26581  rngoneglmul  26582  rngonegrmul  26583  idlnegcl  26647  0idl  26650  0rngo  26652  keridl  26657  smprngopr  26677  fvtresfn  26763  mzpval  26810  mzpindd  26824  pellex  26920  2nn0ind  27030  jm2.26lem3  27094  pw2f1o2val  27132  wepwsolem  27138  fnwe2lem3  27149  lnmfg  27180  dgrsub2  27339  mpaaeu  27355  flcidc  27379  pmtrfrn  27400  mamuvs1  27463  mamuvs2  27464  dvconstbi  27551  stoweidlem26  27775  stoweidlem37  27786  stoweidlem43  27792  stoweidlem50  27799  bnj1006  28991  bnj1110  29012  bnj1253  29047  bnj1280  29050  bnj1463  29085  bnj1312  29088  lubunNEW  29163  lshpne0  29176  lkrval  29278  ldualvaddval  29321  ldualvsval  29328  lub0N  29379  glb0N  29383  opoc1  29392  pmap0  29954  pmap1N  29956  pexmidALTN  30167  trlval2  30352  cdleme31fv  30579  cdlemefrs32fva  30589  cdlemg27b  30885  cdlemk40  31106  erngdvlem4  31180  erng0g  31183  erngdvlem4-rN  31188  dvalveclem  31215  dvh0g  31301  dih0cnv  31473  dih1rn  31477  dih1cnv  31478  doch0  31548  doch1  31549  lcfl7lem  31689  mapdheq  31918  hdmap1eq  31992  hdmapval2lem  32024  hgmapvvlem3  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator