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

Theorem mpdan 672
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 23 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mpan2  675  mpjaodan  793  mpd3an3  1361  eueq2  3251  csbiegf  3425  difsnb  4145  reusv3i  4632  fvtresfn  5966  fvmpt3  5968  ffvelrnd  6038  fnressn  6091  fsnex  6196  f1oiso2  6258  riota5f  6291  onsucuni  6669  wfrlem5  7048  seqomlem2  7176  oaordi  7255  nnaordi  7327  qsdisj  7448  dom2lem  7616  canth2g  7732  limenpsi  7753  php4  7765  onfin  7769  sucxpdom  7787  xpfi  7848  dmfi  7860  pwfilem  7874  pwfi  7875  fiin  7942  supiso  7997  ordiso2  8030  wdom2d  8095  infeq5  8142  cantnfp1lem3  8184  cantnflem1d  8192  rankwflemb  8263  onenon  8382  cardonle  8390  sdomsdomcardi  8404  acni  8474  cardaleph  8518  cdaen  8601  cdainf  8620  infcda1  8621  pwsdompw  8632  infdif  8637  cfval  8675  fin34  8818  fin1a2lem1  8828  fin1a2  8843  ttukeylem6  8942  sdomsdomcard  8983  canth3  8984  fpwwe2  9067  canthwelem  9074  gchcda1  9080  pwfseqlem4  9086  gchcdaidm  9092  gchxpidm  9093  tskwe2  9197  rankcf  9201  tskuni  9207  gruxp  9231  dmrecnq  9392  lterpq  9394  archnq  9404  reclem3pr  9473  reclem4pr  9474  0idsr  9520  lep1  10443  ledivp1  10508  negfi  10554  supaddc  10574  supmul1  10576  suprzcl  11015  uz11  11181  zmin  11260  zbtwnre  11262  rpnnen1lem4  11293  rpnnen1lem5  11294  xnegid  11529  xrsupss  11594  xrinfmss  11595  supxrre  11613  infxrre  11622  infmxrreOLD  11626  eluzfz2  11805  fzsuc  11841  fzsuc2  11851  fzp1disj  11852  fzneuz  11873  fllep1  12034  fraclt1  12035  fracle1  12036  fracge0  12037  flhalf  12059  ceige  12069  ceim1l  12071  fldiv  12084  modval  12095  suppssfz  12203  seqeq1  12213  expubnd  12330  iexpcyc  12376  faclbnd4lem3  12477  faclbnd4lem4  12478  swrdid  12769  swrdccat3blem  12836  cshwn  12884  trclexlem  13037  shftfval  13112  shftcan1  13125  reval  13148  cjmulrcl  13186  addcj  13190  absval  13280  absneg  13319  abscj  13321  sqabsadd  13324  sqabssub  13325  leabs  13341  sqreulem  13401  lo1res  13601  o1of2  13654  o1rlimmul  13660  sumrb  13757  flo1  13890  trirecip  13899  prodrblem2  13963  efcan  14128  efi4p  14169  resin4p  14170  recos4p  14171  sincossq  14208  ruclem10  14269  iddvds  14294  1dvds  14295  2ebits  14395  lcmftp  14571  1idssfct  14592  exprmfct  14610  coprmgcdb  14616  eulerthlem2  14690  odzphi  14701  pcprendvds  14744  pcmpt  14791  vdwlem8  14892  0ram2  14933  prmgaplem7  14981  pwsvscaval  15343  issect2  15601  2initoinv  15847  initoeu1  15848  initoeu2lem1  15851  initoeu2  15853  2termoinv  15854  termoeu1  15855  homarel  15873  joinfval  16189  meetfval  16203  latjcom  16247  latmcom  16263  sgrp2nmndlem5  16605  grprcan  16641  isgrpid2  16644  grpinvid  16659  mulgnn0z  16720  0subg  16784  qus0  16817  ghmker  16850  symginv  16985  pmtrfrn  17041  odmulg2  17135  slwpgp  17191  pj1eq  17276  efgtf  17298  frgpinv  17340  frgpup2  17352  mulgnn0di  17392  cnaddablx  17432  cnaddabl  17433  zaddablx  17434  dprdfadd  17579  dpjidcl  17617  dpjlid  17620  pgpfac1lem3  17636  srgen1zr  17689  ringlz  17743  ringrz  17744  1unit  17812  unitgrpid  17823  1rinv  17833  irredn0  17857  irredneg  17864  isdrng2  17911  abv0  17985  abv1z  17986  abvneg  17988  lsssn0  18097  lspsn0  18157  lsp0  18158  lmhmvsca  18194  lmhmrnlss  18199  lmhmkerlss  18200  lsppratlem5  18300  rsp1  18374  ringen1zr  18427  rlmassa  18476  asclpropd  18496  snifpsrbag  18516  psrvscaval  18542  psrdi  18556  psrdir  18557  mplsubglem  18584  mplvscaval  18598  coe1sclmulfv  18802  ply1idvr1  18812  evl1var  18850  cnfldneg  18920  zringcyg  18982  chrid  19020  chrrhm  19024  ip0r  19126  ocvlss  19157  ocv1  19164  mamuvs1  19352  mamuvs2  19353  matecl  19372  matvscacell  19383  mat0scmat  19485  submaval0  19527  mdetrsca  19550  maduval  19585  minmar1val0  19594  pmatcollpw3fi1lem2  19733  chfacfscmulgsum  19806  chfacfpmmulgsum  19810  chcoeffeqlem  19831  cayleyhamilton0  19835  cayleyhamiltonALT  19837  cctop  19943  cldval  19960  ntrfval  19961  clsfval  19962  cmclsopn  19999  opncldf3  20024  neifval  20037  lpfval  20076  cnrmnrm  20299  islocfin  20454  tx1cn  20546  tx2cn  20547  idqtop  20643  kqtopon  20664  kqid  20665  kqcld  20672  hmphen2  20736  filssufil  20849  ufileu  20856  alexsublem  20981  symgtgp  21038  ustuqtop4  21181  ustuqtop5  21182  cstucnd  21221  metustexhalf  21493  nm0  21562  rlmnlm  21613  nmolb  21640  metdseq0  21773  iocopnst  21855  pi1xfrval  21969  clmvneg1  22006  ipcau2  22092  tchcphlem1  22093  tchcphlem2  22094  cmetcaulem  22142  ovolicc2lem3  22341  ovolicc2lem4  22342  mbfmulc2lem  22471  i1fpos  22532  mbfi1fseqlem3  22543  mbfi1fseqlem4  22544  itg2ge0  22561  dvres2  22735  dvaddbr  22760  dvmulbr  22761  dvcobr  22768  dvfsumlem4  22849  ftc1a  22857  ftc1lem6  22861  uc1pmon1p  22968  ig1pval2  22990  dgradd2  23081  dgrcolem2  23087  plydivlem4  23108  plydiveu  23110  elqaalem3  23133  qaa  23135  ulmdvlem1  23211  abelthlem6  23247  abelthlem7  23249  eflogeq  23407  jensenlem2  23769  harmonicbnd4  23792  sgmnncl  23928  dchrptlem2  24047  1lgs  24119  lgs1  24120  dchrisumlem2  24182  dchrisum0lem2a  24209  selberg2lem  24242  pntrsumo1  24257  pntrsumbnd  24258  pntpbnd1  24278  pntlemr  24294  pntlemj  24295  padicabvf  24323  istrkg3ld  24363  tglineeltr  24526  cusgraexilem2  25031  cusgraexi  25032  cusgrasizeinds  25040  wwlksubclwwlk  25368  erclwwlkref  25377  erclwwlknref  25389  eupacl  25533  eupapf  25536  eupaseg  25537  frgrancvvdeqlemC  25603  frghash2spot  25627  isgrpoi  25762  grpoinvfval  25788  grpoinvid  25796  grpodivfval  25806  gxfval  25821  gxid  25837  issubgo  25867  cnaddablo  25914  ghomidOLD  25929  rngolz  25965  rngorz  25966  rngosn6  25992  vcz  26025  vcoprne  26034  nvz0  26133  sspz  26210  lno0  26233  nmobndi  26252  ipasslem2  26309  shunssi  26847  ococin  26887  ssjo  26926  pjocini  27177  nlfnval  27360  lncnopbd  27516  riesz3i  27541  cnlnadjlem7  27552  pjclem4  27678  pj3si  27686  hstoc  27701  hstnmoc  27702  hstoh  27711  hst0  27712  mdsl2i  27801  chirredlem3  27871  chirredlem4  27872  dmdbr5ati  27901  rexunirn  27953  fcnvgreu  28106  infxrge0glb  28177  2sqcoprm  28237  omndmul2  28304  omndmul  28306  isarchi3  28333  orng0le1  28405  esumcvg  28737  esumcvgre  28742  sigaval  28762  unelldsys  28810  fiunelros  28826  measval  28850  pmeasmono  28976  eulerpartlemgvv  29026  probfinmeasb  29079  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemsi  29164  ballotlemfrci  29177  sgnneg  29190  signlem0  29255  bnj1006  29549  bnj1110  29570  bnj1253  29605  bnj1280  29608  bnj1463  29643  bnj1312  29646  erdszelem7  29699  erdszelem8  29700  cvmliftlem10  29796  cvmliftlem13  29798  cvmlift2lem9  29813  cvmlift3lem6  29826  cvmlift3lem7  29827  cvmlift3lem9  29829  ghomgrpilem2  30083  dfrdg2  30220  dftrpred3g  30252  frrlem5  30296  bdayval  30313  cldregopn  30763  tailfval  30804  filnetlem3  30812  filnetlem4  30813  ontopbas  30864  f1omptsnlem  31463  icoreunrn  31487  relowlpssretop  31492  wl-sbal2  31592  poimirlem1  31635  poimirlem2  31636  poimirlem4  31638  poimirlem6  31640  poimirlem7  31641  poimirlem11  31645  poimirlem12  31646  poimirlem17  31651  poimirlem20  31654  poimirlem22  31656  poimirlem23  31657  poimirlem28  31662  poimir  31667  ismblfin  31675  cnambfre  31683  bddiblnc  31706  ftc1cnnc  31710  dvasin  31722  ismtyres  31834  heiborlem8  31844  rngonegmn1l  31882  rngonegmn1r  31883  rngoneglmul  31884  rngonegrmul  31885  idlnegcl  31949  0idl  31952  0rngo  31954  keridl  31959  smprngopr  31979  lshpne0  32251  lkrval  32353  ldualvaddval  32396  ldualvsval  32403  opoc1  32467  pmap0  33029  pmap1N  33031  pexmidALTN  33242  cdleme31fv  33656  cdlemg27b  33962  erngdvlem4  34257  erng0g  34260  erngdvlem4-rN  34265  dvalveclem  34292  dvh0g  34378  dih0cnv  34550  dih1rn  34554  dih1cnv  34555  doch0  34625  doch1  34626  lcfl7lem  34766  mapdheq  34995  hdmap1eq  35069  hdmapval2lem  35101  hgmapvvlem3  35195  mzpval  35273  mzpindd  35287  pellex  35379  2nn0ind  35489  jm2.26lem3  35552  pw2f1o2val  35590  wepwsolem  35596  fnwe2lem3  35606  lnmfg  35636  dgrsub2  35690  mpaaeu  35705  flcidc  35729  suprleubrd  36236  suprlubrd  36240  imo72b2  36246  dvconstbi  36310  bcc0  36316  binomcxplemnotnn0  36332  nnfoctb  37013  sumnnodd  37272  icccncfext  37327  itgsin0pilem1  37385  stoweidlem22  37441  stoweidlem32  37452  stoweidlem35  37455  stoweidlem36  37456  stoweidlem37  37457  stoweidlem43  37463  stoweidlem50  37470  wallispilem5  37490  stirlinglem2  37496  stirlinglem3  37497  stirlinglem4  37498  stirlinglem8  37502  stirlinglem11  37505  stirlinglem12  37506  stirlinglem14  37508  stirlinglem15  37509  fourierdlem11  37539  fourierdlem20  37548  fourierdlem21  37549  fourierdlem41  37569  fourierdlem42  37570  fourierdlem48  37576  fourierdlem49  37577  fourierdlem64  37592  fourierdlem71  37599  fourierdlem79  37607  fourierdlem90  37618  fourierdlem91  37619  fourierswlem  37652  etransclem17  37673  etransclem38  37694  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbnd  38284  pfxid  38313  pfx2  38333  usgrauvtxvd  38418  vdcusgra  38419  usgedgvadf1lem2  38474  usgedgvadf1ALTlem2  38477  isclintop  38591  clintopcllaw  38595  nzrneg1ne0  38617  rnglz  38632  c0snmgmhm  38662  zrrnghm  38665  lidldomn1  38669  uzlidlring  38677  2zrngnmlid  38697  cznrng  38705  zrinitorngc  38750  zrtermorngc  38751  zrtermoringc  38820  coe1id  38926  blenre  39136  blennn  39137
  Copyright terms: Public domain W3C validator