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

Theorem mpdan 650
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 20 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan2  653  mpjaodan  762  mpd3an3  1280  eueq2  3068  csbiegf  3251  difsnb  3900  reusv3i  4689  onsucuni  4767  fvmpt3  5767  ffvelrnd  5830  fnressn  5877  f1oiso2  6031  riota5f  6533  riotasvdOLD  6552  seqomlem2  6667  oaordi  6748  nnaordi  6820  qsdisj  6940  dom2lem  7106  canth2g  7220  limenpsi  7241  php4  7253  onfin  7256  sucxpdom  7277  xpfi  7337  dmfi  7348  pwfilem  7359  pwfi  7360  fiin  7385  supiso  7433  ordiso2  7440  wemaplem2  7472  wdom2d  7504  infeq5  7548  cantnfp1lem3  7592  cantnflem1d  7600  r1val1  7668  rankwflemb  7675  onenon  7792  cardonle  7800  sdomsdomcardi  7814  acni  7882  cardaleph  7926  cdaen  8009  cdainf  8028  infcda1  8029  pwsdompw  8040  infdif  8045  cfval  8083  fin34  8226  fin1a2lem1  8236  fin1a2  8251  ttukeylem6  8350  sdomsdomcard  8391  canth3  8392  fpwwe2  8474  canthwelem  8481  gchcda1  8487  pwfseqlem4  8493  gchcdaidm  8499  gchxpidm  8500  tskwe2  8604  rankcf  8608  tskuni  8614  gruxp  8638  dmrecnq  8801  lterpq  8803  archnq  8813  reclem3pr  8882  reclem4pr  8883  0idsr  8928  lep1  9805  ledivp1  9868  supmul1  9929  suprzcl  10305  uz11  10464  zmin  10526  zbtwnre  10528  rpnnen1lem4  10559  rpnnen1lem5  10560  xnegid  10778  xleadd1a  10788  xlt2add  10795  xmullem  10799  xmulgt0  10818  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  xadddi  10830  xadddi2  10832  xrsupss  10843  xrinfmss  10844  supxrre  10862  infmxrre  10870  eluzfz2  11021  fzsuc  11052  fzsuc2  11060  fzp1disj  11061  fzneuz  11083  fllep1  11165  fraclt1  11166  fracle1  11167  fracge0  11168  flhalf  11186  ceige  11188  ceim1l  11189  fldiv  11196  modval  11207  seqeq1  11281  expubnd  11395  iexpcyc  11440  faclbnd4lem3  11541  faclbnd4lem4  11542  shftfval  11840  shftcan1  11853  reval  11866  cjmulrcl  11904  addcj  11908  absval  11998  absneg  12037  abscj  12039  sqabsadd  12042  sqabssub  12043  leabs  12059  sqreulem  12118  lo1res  12308  o1of2  12361  o1rlimmul  12367  sumrb  12462  flo1  12589  trirecip  12597  efcan  12652  efi4p  12693  resin4p  12694  recos4p  12695  sincossq  12732  ruclem10  12793  iddvds  12818  1dvds  12819  2ebits  12914  1idssfct  13040  exprmfct  13065  eulerthlem2  13126  odzphi  13137  pcprendvds  13169  pcmpt  13216  vdwlem8  13311  0ram2  13344  pwsvscaval  13672  issect2  13935  homarel  14146  latjcom  14443  latlej1  14444  latlej2  14445  latmcom  14459  latmle1  14460  latmle2  14461  grprcan  14793  isgrpid2  14796  grpinvid  14811  mulgnn0z  14865  0subg  14920  divs0  14953  ghmker  14986  symginv  15060  odval2  15144  odmulg2  15146  slwpgp  15202  pj1eq  15287  efgtf  15309  frgpinv  15351  frgpup2  15363  mulgnn0di  15403  cnaddablx  15436  cnaddabl  15437  zaddablx  15438  dprdfadd  15533  dpjidcl  15571  dpjlid  15574  pgpfac1lem3  15590  rnglz  15655  rngrz  15656  1unit  15718  unitgrpid  15729  1rinv  15739  irredn0  15763  irredneg  15770  isdrng2  15800  abv0  15874  abv1z  15875  abvneg  15877  lsssn0  15979  lspsn0  16039  lsp0  16040  lmhmvsca  16076  lmhmrnlss  16081  lmhmkerlss  16082  lsppratlem5  16178  rsp1  16250  rlmassa  16340  asclpropd  16359  psrvscaval  16411  psrdi  16425  psrdir  16426  mplsubglem  16453  mplvscaval  16466  coe1sclmulfv  16630  cnfldneg  16682  zcyg  16727  chrid  16763  chrrhm  16767  ip0r  16823  ocvlss  16854  ocv1  16861  cctop  17025  cldval  17042  ntrfval  17043  clsfval  17044  cmclsopn  17081  opncldf3  17105  neifval  17118  lpfval  17157  cnrmnrm  17379  tx1cn  17594  tx2cn  17595  idqtop  17691  kqtopon  17712  kqid  17713  kqcld  17720  hmphen2  17784  filssufil  17897  ufileu  17904  alexsublem  18028  symgtgp  18084  ustuqtop4  18227  ustuqtop5  18228  cstucnd  18267  isxmet2d  18310  metustexhalfOLD  18546  metustexhalf  18547  nm0  18626  rlmnlm  18677  nmolb  18704  metdseq0  18837  iocopnst  18918  icccvx  18928  pi1xfrval  19032  clmvneg1  19069  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  cmetcaulem  19194  ivthicc  19308  ovolicc2lem3  19368  ovolicc2lem4  19369  mbfmulc2lem  19492  i1fpos  19551  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  itg2ge0  19580  dvres2  19752  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  c1lip1  19834  dvivth  19847  dvfsumlem4  19866  ftc1a  19874  ftc1lem6  19878  evl1var  19905  uc1pmon1p  20027  ig1pval2  20049  dgradd2  20139  dgrcolem2  20145  plydivlem4  20166  plydiveu  20168  elqaalem3  20191  qaa  20193  ulmdvlem1  20269  abelthlem6  20305  abelthlem7  20307  reeff1o  20316  coseq00topi  20363  tanabsge  20367  eflogeq  20449  logcnlem3  20488  atantan  20716  atanbnd  20719  cvxcl  20776  jensenlem2  20779  harmonicbnd4  20802  sgmnncl  20883  dchrptlem2  21002  1lgs  21074  lgs1  21075  dchrisumlem2  21137  dchrisum0lem2a  21164  selberg2lem  21197  pntrsumo1  21212  pntrsumbnd  21213  pntpbnd1  21233  pntlemr  21249  pntlemj  21250  ostthlem1  21274  padicabvf  21278  cusgraexilem2  21429  cusgraexi  21430  cusgrasizeinds  21438  eupacl  21644  eupapf  21647  eupaseg  21648  isgrpoi  21739  grpoinvfval  21765  grpoinvid  21773  grpodivfval  21783  gxfval  21798  gxid  21814  issubgo  21844  cnaddablo  21891  ghomid  21906  rngolz  21942  rngorz  21943  rngosn6  21969  vcz  22002  vcoprne  22011  nvz0  22110  sspz  22187  lno0  22210  nmobndi  22229  ipasslem2  22286  shunssi  22823  ococin  22863  ssjo  22902  pjocini  23153  nlfnval  23337  lncnopbd  23493  riesz3i  23518  cnlnadjlem7  23529  pjclem4  23655  pj3si  23663  hstoc  23678  hstnmoc  23679  hstoh  23688  hst0  23689  mdsl2i  23778  chirredlem3  23848  chirredlem4  23849  dmdbr5ati  23878  rexunirn  23931  abfmpel  24020  xrpxdivcld  24134  ofld0le1  24195  esumcst  24408  esumcvg  24429  sigaval  24446  measval  24505  probfinmeasb  24640  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsi  24725  ballotlemfrci  24738  erdszelem7  24836  erdszelem8  24837  cvmliftlem10  24934  cvmliftlem13  24936  cvmlift2lem9  24951  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  ghomgrpilem2  25050  prodrblem2  25210  dfrdg2  25366  dftrpred3g  25450  wfrlem5  25474  frrlem5  25499  bdayval  25516  ontopbas  26082  supaddc  26137  ismblfin  26146  cnambfre  26154  bddiblnc  26174  ftc1cnnc  26178  cldregopn  26224  islocfin  26266  tailfval  26291  filnetlem3  26299  filnetlem4  26300  ismtyres  26407  heiborlem8  26417  rngonegmn1l  26455  rngonegmn1r  26456  rngoneglmul  26457  rngonegrmul  26458  idlnegcl  26522  0idl  26525  0rngo  26527  keridl  26532  smprngopr  26552  fvtresfn  26634  mzpval  26679  mzpindd  26693  pellex  26788  2nn0ind  26898  jm2.26lem3  26962  pw2f1o2val  27000  wepwsolem  27006  fnwe2lem3  27017  lnmfg  27048  dgrsub2  27207  mpaaeu  27223  flcidc  27247  pmtrfrn  27268  mamuvs1  27331  mamuvs2  27332  dvconstbi  27419  itgsin0pilem1  27611  stoweidlem22  27638  stoweidlem32  27648  stoweidlem35  27651  stoweidlem36  27652  stoweidlem37  27653  stoweidlem43  27659  stoweidlem50  27666  wallispilem5  27685  stirlinglem2  27691  stirlinglem3  27692  stirlinglem4  27693  stirlinglem8  27697  stirlinglem11  27700  stirlinglem12  27701  stirlinglem14  27703  stirlinglem15  27704  frgrancvvdeqlemC  28142  frghash2spot  28166  bnj1006  29036  bnj1110  29057  bnj1253  29092  bnj1280  29095  bnj1463  29130  bnj1312  29133  lubunNEW  29456  lshpne0  29469  lkrval  29571  ldualvaddval  29614  ldualvsval  29621  lub0N  29672  glb0N  29676  opoc1  29685  pmap0  30247  pmap1N  30249  pexmidALTN  30460  trlval2  30645  cdleme31fv  30872  cdlemefrs32fva  30882  cdlemg27b  31178  cdlemk40  31399  erngdvlem4  31473  erng0g  31476  erngdvlem4-rN  31481  dvalveclem  31508  dvh0g  31594  dih0cnv  31766  dih1rn  31770  dih1cnv  31771  doch0  31841  doch1  31842  lcfl7lem  31982  mapdheq  32211  hdmap1eq  32285  hdmapval2lem  32317  hgmapvvlem3  32411
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 178  df-an 361
  Copyright terms: Public domain W3C validator