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  3015  csbiegf  3197  difsnb  3836  reusv3i  4620  onsucuni  4698  fvmpt3  5684  ffvelrnd  5746  fnressn  5786  f1oiso2  5933  riota5f  6413  riotasvdOLD  6432  seqomlem2  6547  oaordi  6628  nnaordi  6700  qsdisj  6820  dom2lem  6986  canth2g  7100  limenpsi  7121  php4  7133  onfin  7136  sucxpdom  7157  xpfi  7215  dmfi  7226  pwfilem  7237  pwfi  7238  fiin  7262  supiso  7310  ordiso2  7317  wemaplem2  7349  wdom2d  7381  infeq5  7425  cantnfp1lem3  7469  cantnflem1d  7477  r1val1  7545  rankwflemb  7552  onenon  7669  cardonle  7677  sdomsdomcardi  7691  acni  7759  cardaleph  7803  cdaen  7886  cdainf  7905  infcda1  7906  pwsdompw  7917  infdif  7922  cfval  7960  fin34  8103  fin1a2lem1  8113  fin1a2  8128  ttukeylem6  8228  sdomsdomcard  8269  canth3  8270  fpwwe2  8352  canthwelem  8359  gchcda1  8365  pwfseqlem4  8371  gchcdaidm  8377  gchxpidm  8378  tskwe2  8482  rankcf  8486  tskuni  8492  gruxp  8516  dmrecnq  8679  lterpq  8681  archnq  8691  reclem3pr  8760  reclem4pr  8761  0idsr  8806  lep1  9682  ledivp1  9745  supmul1  9806  suprzcl  10180  uz11  10339  zmin  10401  zbtwnre  10403  rpnnen1lem4  10434  rpnnen1lem5  10435  xnegid  10652  xleadd1a  10662  xlt2add  10669  xmullem  10673  xmulgt0  10692  xmulasslem3  10695  xlemul1a  10697  xadddilem  10703  xadddi  10704  xadddi2  10706  xrsupss  10716  xrinfmss  10717  supxrre  10735  infmxrre  10743  eluzfz2  10893  fzsuc  10924  fzsuc2  10931  fzp1disj  10932  fzneuz  10952  fllep1  11022  fraclt1  11023  fracle1  11024  fracge0  11025  flhalf  11043  ceige  11045  ceim1l  11046  fldiv  11053  modval  11064  seqeq1  11138  expubnd  11252  iexpcyc  11297  faclbnd4lem3  11398  faclbnd4lem4  11399  shftfval  11655  shftcan1  11668  reval  11681  cjmulrcl  11719  addcj  11723  absval  11813  absneg  11852  abscj  11854  sqabsadd  11857  sqabssub  11858  leabs  11874  sqreulem  11933  lo1res  12123  o1of2  12176  o1rlimmul  12182  sumrb  12277  flo1  12404  trirecip  12412  efcan  12467  efi4p  12508  resin4p  12509  recos4p  12510  sincossq  12547  ruclem10  12608  iddvds  12633  1dvds  12634  2ebits  12729  1idssfct  12855  exprmfct  12880  eulerthlem2  12941  odzphi  12952  pcprendvds  12984  pcmpt  13031  vdwlem8  13126  0ram2  13159  pwsvscaval  13487  issect2  13750  homarel  13961  latjcom  14258  latlej1  14259  latlej2  14260  latmcom  14274  latmle1  14275  latmle2  14276  lubun  14320  grprcan  14608  isgrpid2  14611  grpinvid  14626  mulgnn0z  14680  0subg  14735  divs0  14768  ghmker  14801  symginv  14875  odval2  14959  odmulg2  14961  slwpgp  15017  pj1eq  15102  efgtf  15124  frgpinv  15166  frgpup2  15178  mulgnn0di  15218  cnaddablx  15251  cnaddabl  15252  zaddablx  15253  dprdfadd  15348  dpjidcl  15386  dpjlid  15389  pgpfac1lem3  15405  rnglz  15470  rngrz  15471  1unit  15533  unitgrpid  15544  1rinv  15554  irredn0  15578  irredneg  15585  isdrng2  15615  abv0  15689  abv1z  15690  abvneg  15692  lsssn0  15798  lspsn0  15858  lsp0  15859  lmhmvsca  15895  lmhmrnlss  15900  lmhmkerlss  15901  lsppratlem5  15997  rsp1  16069  rlmassa  16159  asclpropd  16178  psrvscaval  16230  psrdi  16244  psrdir  16245  mplsubglem  16272  mplvscaval  16285  coe1sclmulfv  16452  cnfldneg  16500  zcyg  16545  chrid  16581  chrrhm  16585  ip0r  16641  ocvlss  16672  ocv1  16679  cctop  16843  cldval  16860  ntrfval  16861  clsfval  16862  cmclsopn  16899  opncldf3  16923  neifval  16936  lpfval  16970  cnrmnrm  17189  tx1cn  17403  tx2cn  17404  idqtop  17497  kqtopon  17518  kqid  17519  kqcld  17526  hmphen2  17590  filssufil  17703  ufileu  17710  alexsublem  17834  symgtgp  17880  isxmet2d  17988  nm0  18244  rlmnlm  18295  nmolb  18322  metdseq0  18455  iocopnst  18536  icccvx  18546  pi1xfrval  18650  clmvneg1  18687  ipcau2  18762  tchcphlem1  18763  tchcphlem2  18764  cmetcaulem  18812  ivthicc  18916  ovolicc2lem3  18976  ovolicc2lem4  18977  mbfmulc2lem  19100  i1fpos  19159  mbfi1fseqlem3  19170  mbfi1fseqlem4  19171  itg2ge0  19188  dvres2  19360  dvaddbr  19385  dvmulbr  19386  dvcobr  19393  c1lip1  19442  dvivth  19455  dvfsumlem4  19474  ftc1a  19482  ftc1lem6  19486  evl1var  19513  uc1pmon1p  19635  ig1pval2  19657  dgradd2  19747  dgrcolem2  19753  plydivlem4  19774  plydiveu  19776  elqaalem3  19799  qaa  19801  ulmdvlem1  19877  abelthlem6  19913  abelthlem7  19915  reeff1o  19924  coseq00topi  19971  tanabsge  19975  eflogeq  20057  logcnlem3  20096  atantan  20324  atanbnd  20327  cvxcl  20384  jensenlem2  20387  harmonicbnd4  20410  sgmnncl  20491  dchrptlem2  20610  1lgs  20682  lgs1  20683  dchrisumlem2  20745  dchrisum0lem2a  20772  selberg2lem  20805  pntrsumo1  20820  pntrsumbnd  20821  pntpbnd1  20841  pntlemr  20857  pntlemj  20858  ostthlem1  20882  padicabvf  20886  isgrpoi  20971  grpoinvfval  20997  grpoinvid  21005  grpodivfval  21015  gxfval  21030  gxid  21046  issubgo  21076  cnaddablo  21123  ghomid  21138  rngolz  21174  rngorz  21175  rngosn6  21201  vcz  21234  vcoprne  21243  nvz0  21342  sspz  21419  lno0  21442  nmobndi  21461  ipasslem2  21518  shunssi  22055  ococin  22095  ssjo  22134  pjocini  22385  nlfnval  22569  adjvalval  22625  lncnopbd  22725  riesz3i  22750  cnlnadjlem7  22761  pjclem4  22887  pj3si  22895  hstoc  22910  hstnmoc  22911  hstoh  22920  hst0  22921  mdsl2i  23010  chirredlem3  23080  chirredlem4  23081  dmdbr5ati  23110  rexunirn  23167  abfmpel  23267  xrpxdivcld  23386  ustuqtop4  23548  ustuqtop5  23549  cstucnd  23579  metustto  23597  metustexhalf  23600  metustfbas  23601  qqh0  23641  qqh1  23642  rnlogblem  23665  esumcst  23721  esumcvg  23742  sigaval  23759  measval  23818  measiuns  23835  sxbrsigalem0  23885  probfinmeasb  23936  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemsi  24021  ballotlemfrci  24034  erdszelem7  24132  erdszelem8  24133  cvmliftlem10  24229  cvmliftlem13  24231  cvmlift2lem9  24246  cvmlift3lem6  24259  cvmlift3lem7  24260  cvmlift3lem9  24262  eupacl  24288  eupapf  24291  eupaseg  24292  ghomgrpilem2  24397  prodrblem2  24558  dfrdg2  24710  dftrpred3g  24794  wfrlem5  24818  frrlem5  24843  bdayval  24860  ontopbas  25426  supaddc  25482  itg2addnc  25494  bddiblnc  25510  ftc1cnnc  25514  cldregopn  25573  islocfin  25620  tailfval  25645  filnetlem3  25653  filnetlem4  25654  ismtyres  25855  heiborlem8  25865  rngonegmn1l  25903  rngonegmn1r  25904  rngoneglmul  25905  rngonegrmul  25906  idlnegcl  25970  0idl  25973  0rngo  25975  keridl  25980  smprngopr  26000  fvtresfn  26086  mzpval  26133  mzpindd  26147  pellex  26243  2nn0ind  26353  jm2.26lem3  26417  pw2f1o2val  26455  wepwsolem  26461  fnwe2lem3  26472  lnmfg  26503  dgrsub2  26662  mpaaeu  26678  flcidc  26702  pmtrfrn  26723  mamuvs1  26786  mamuvs2  26787  dvconstbi  26874  stoweidlem26  27098  stoweidlem37  27109  stoweidlem43  27115  stoweidlem50  27122  cusgraexilem2  27622  cusgraexi  27623  cusgrasizeinds  27631  frgrancvvdeqlemC  27855  bnj1006  28736  bnj1110  28757  bnj1253  28792  bnj1280  28795  bnj1463  28830  bnj1312  28833  lubunNEW  29215  lshpne0  29228  lkrval  29330  ldualvaddval  29373  ldualvsval  29380  lub0N  29431  glb0N  29435  opoc1  29444  pmap0  30006  pmap1N  30008  pexmidALTN  30219  trlval2  30404  cdleme31fv  30631  cdlemefrs32fva  30641  cdlemg27b  30937  cdlemk40  31158  erngdvlem4  31232  erng0g  31235  erngdvlem4-rN  31240  dvalveclem  31267  dvh0g  31353  dih0cnv  31525  dih1rn  31529  dih1cnv  31530  doch0  31600  doch1  31601  lcfl7lem  31741  mapdheq  31970  hdmap1eq  32044  hdmapval2lem  32076  hgmapvvlem3  32170
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