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

Theorem mpdan 651
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 21 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpan2  654  mpjaodan  763  mpd3an3  1281  eueq2  3110  csbiegf  3293  difsnb  3942  reusv3i  4732  onsucuni  4810  fvmpt3  5810  ffvelrnd  5873  fnressn  5920  f1oiso2  6074  riota5f  6576  riotasvdOLD  6595  seqomlem2  6710  oaordi  6791  nnaordi  6863  qsdisj  6983  dom2lem  7149  canth2g  7263  limenpsi  7284  php4  7296  onfin  7299  sucxpdom  7320  xpfi  7380  dmfi  7391  pwfilem  7403  pwfi  7404  fiin  7429  supiso  7479  ordiso2  7486  wemaplem2  7518  wdom2d  7550  infeq5  7594  cantnfp1lem3  7638  cantnflem1d  7646  r1val1  7714  rankwflemb  7721  onenon  7838  cardonle  7846  sdomsdomcardi  7860  acni  7928  cardaleph  7972  cdaen  8055  cdainf  8074  infcda1  8075  pwsdompw  8086  infdif  8091  cfval  8129  fin34  8272  fin1a2lem1  8282  fin1a2  8297  ttukeylem6  8396  sdomsdomcard  8437  canth3  8438  fpwwe2  8520  canthwelem  8527  gchcda1  8533  pwfseqlem4  8539  gchcdaidm  8545  gchxpidm  8546  tskwe2  8650  rankcf  8654  tskuni  8660  gruxp  8684  dmrecnq  8847  lterpq  8849  archnq  8859  reclem3pr  8928  reclem4pr  8929  0idsr  8974  lep1  9851  ledivp1  9914  supmul1  9975  suprzcl  10351  uz11  10510  zmin  10572  zbtwnre  10574  rpnnen1lem4  10605  rpnnen1lem5  10606  xnegid  10824  xleadd1a  10834  xlt2add  10841  xmullem  10845  xmulgt0  10864  xmulasslem3  10867  xlemul1a  10869  xadddilem  10875  xadddi  10876  xadddi2  10878  xrsupss  10889  xrinfmss  10890  supxrre  10908  infmxrre  10916  eluzfz2  11067  fzsuc  11098  fzsuc2  11106  fzp1disj  11107  fzneuz  11130  fllep1  11212  fraclt1  11213  fracle1  11214  fracge0  11215  flhalf  11233  ceige  11235  ceim1l  11236  fldiv  11243  modval  11254  seqeq1  11328  expubnd  11442  iexpcyc  11487  faclbnd4lem3  11588  faclbnd4lem4  11589  shftfval  11887  shftcan1  11900  reval  11913  cjmulrcl  11951  addcj  11955  absval  12045  absneg  12084  abscj  12086  sqabsadd  12089  sqabssub  12090  leabs  12106  sqreulem  12165  lo1res  12355  o1of2  12408  o1rlimmul  12414  sumrb  12509  flo1  12636  trirecip  12644  efcan  12699  efi4p  12740  resin4p  12741  recos4p  12742  sincossq  12779  ruclem10  12840  iddvds  12865  1dvds  12866  2ebits  12961  1idssfct  13087  exprmfct  13112  eulerthlem2  13173  odzphi  13184  pcprendvds  13216  pcmpt  13263  vdwlem8  13358  0ram2  13391  pwsvscaval  13719  issect2  13982  homarel  14193  latjcom  14490  latlej1  14491  latlej2  14492  latmcom  14506  latmle1  14507  latmle2  14508  grprcan  14840  isgrpid2  14843  grpinvid  14858  mulgnn0z  14912  0subg  14967  divs0  15000  ghmker  15033  symginv  15107  odval2  15191  odmulg2  15193  slwpgp  15249  pj1eq  15334  efgtf  15356  frgpinv  15398  frgpup2  15410  mulgnn0di  15450  cnaddablx  15483  cnaddabl  15484  zaddablx  15485  dprdfadd  15580  dpjidcl  15618  dpjlid  15621  pgpfac1lem3  15637  rnglz  15702  rngrz  15703  1unit  15765  unitgrpid  15776  1rinv  15786  irredn0  15810  irredneg  15817  isdrng2  15847  abv0  15921  abv1z  15922  abvneg  15924  lsssn0  16026  lspsn0  16086  lsp0  16087  lmhmvsca  16123  lmhmrnlss  16128  lmhmkerlss  16129  lsppratlem5  16225  rsp1  16297  rlmassa  16387  asclpropd  16406  psrvscaval  16458  psrdi  16472  psrdir  16473  mplsubglem  16500  mplvscaval  16513  coe1sclmulfv  16677  cnfldneg  16729  zcyg  16774  chrid  16810  chrrhm  16814  ip0r  16870  ocvlss  16901  ocv1  16908  cctop  17072  cldval  17089  ntrfval  17090  clsfval  17091  cmclsopn  17128  opncldf3  17152  neifval  17165  lpfval  17204  cnrmnrm  17427  tx1cn  17643  tx2cn  17644  idqtop  17740  kqtopon  17761  kqid  17762  kqcld  17769  hmphen2  17833  filssufil  17946  ufileu  17953  alexsublem  18077  symgtgp  18133  ustuqtop4  18276  ustuqtop5  18277  cstucnd  18316  isxmet2d  18359  metustexhalfOLD  18595  metustexhalf  18596  nm0  18675  rlmnlm  18726  nmolb  18753  metdseq0  18886  iocopnst  18967  icccvx  18977  pi1xfrval  19081  clmvneg1  19118  ipcau2  19193  tchcphlem1  19194  tchcphlem2  19195  cmetcaulem  19243  ivthicc  19357  ovolicc2lem3  19417  ovolicc2lem4  19418  mbfmulc2lem  19541  i1fpos  19600  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  itg2ge0  19629  dvres2  19801  dvaddbr  19826  dvmulbr  19827  dvcobr  19834  c1lip1  19883  dvivth  19896  dvfsumlem4  19915  ftc1a  19923  ftc1lem6  19927  evl1var  19954  uc1pmon1p  20076  ig1pval2  20098  dgradd2  20188  dgrcolem2  20194  plydivlem4  20215  plydiveu  20217  elqaalem3  20240  qaa  20242  ulmdvlem1  20318  abelthlem6  20354  abelthlem7  20356  reeff1o  20365  coseq00topi  20412  tanabsge  20416  eflogeq  20498  logcnlem3  20537  atantan  20765  atanbnd  20768  cvxcl  20825  jensenlem2  20828  harmonicbnd4  20851  sgmnncl  20932  dchrptlem2  21051  1lgs  21123  lgs1  21124  dchrisumlem2  21186  dchrisum0lem2a  21213  selberg2lem  21246  pntrsumo1  21261  pntrsumbnd  21262  pntpbnd1  21282  pntlemr  21298  pntlemj  21299  ostthlem1  21323  padicabvf  21327  cusgraexilem2  21478  cusgraexi  21479  cusgrasizeinds  21487  eupacl  21693  eupapf  21696  eupaseg  21697  isgrpoi  21788  grpoinvfval  21814  grpoinvid  21822  grpodivfval  21832  gxfval  21847  gxid  21863  issubgo  21893  cnaddablo  21940  ghomid  21955  rngolz  21991  rngorz  21992  rngosn6  22018  vcz  22051  vcoprne  22060  nvz0  22159  sspz  22236  lno0  22259  nmobndi  22278  ipasslem2  22335  shunssi  22872  ococin  22912  ssjo  22951  pjocini  23202  nlfnval  23386  lncnopbd  23542  riesz3i  23567  cnlnadjlem7  23578  pjclem4  23704  pj3si  23712  hstoc  23727  hstnmoc  23728  hstoh  23737  hst0  23738  mdsl2i  23827  chirredlem3  23897  chirredlem4  23898  dmdbr5ati  23927  rexunirn  23980  abfmpel  24069  xrpxdivcld  24183  ofld0le1  24244  esumcst  24457  esumcvg  24478  sigaval  24495  measval  24554  probfinmeasb  24689  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemsi  24774  ballotlemfrci  24787  erdszelem7  24885  erdszelem8  24886  cvmliftlem10  24983  cvmliftlem13  24985  cvmlift2lem9  25000  cvmlift3lem6  25013  cvmlift3lem7  25014  cvmlift3lem9  25016  ghomgrpilem2  25099  prodrblem2  25259  dfrdg2  25425  dftrpred3g  25513  wfrlem5  25544  frrlem5  25588  bdayval  25605  ontopbas  26180  supaddc  26239  ismblfin  26249  cnambfre  26257  bddiblnc  26277  ftc1cnnc  26281  cldregopn  26336  islocfin  26378  tailfval  26403  filnetlem3  26411  filnetlem4  26412  ismtyres  26519  heiborlem8  26529  rngonegmn1l  26567  rngonegmn1r  26568  rngoneglmul  26569  rngonegrmul  26570  idlnegcl  26634  0idl  26637  0rngo  26639  keridl  26644  smprngopr  26664  fvtresfn  26746  mzpval  26791  mzpindd  26805  pellex  26900  2nn0ind  27010  jm2.26lem3  27074  pw2f1o2val  27112  wepwsolem  27118  fnwe2lem3  27129  lnmfg  27159  dgrsub2  27318  mpaaeu  27334  flcidc  27358  pmtrfrn  27379  mamuvs1  27442  mamuvs2  27443  dvconstbi  27530  itgsin0pilem1  27722  stoweidlem22  27749  stoweidlem32  27759  stoweidlem35  27762  stoweidlem36  27763  stoweidlem37  27764  stoweidlem43  27770  stoweidlem50  27777  wallispilem5  27796  stirlinglem2  27802  stirlinglem3  27803  stirlinglem4  27804  stirlinglem8  27808  stirlinglem11  27811  stirlinglem12  27812  stirlinglem14  27814  stirlinglem15  27815  swrdccat3blem  28240  cshwn  28261  usgrauvtxvd  28416  vdcusgra  28417  frgrancvvdeqlemC  28490  frghash2spot  28514  bnj1006  29392  bnj1110  29413  bnj1253  29448  bnj1280  29451  bnj1463  29486  bnj1312  29489  lubunNEW  29833  lshpne0  29846  lkrval  29948  ldualvaddval  29991  ldualvsval  29998  lub0N  30049  glb0N  30053  opoc1  30062  pmap0  30624  pmap1N  30626  pexmidALTN  30837  trlval2  31022  cdleme31fv  31249  cdlemefrs32fva  31259  cdlemg27b  31555  cdlemk40  31776  erngdvlem4  31850  erng0g  31853  erngdvlem4-rN  31858  dvalveclem  31885  dvh0g  31971  dih0cnv  32143  dih1rn  32147  dih1cnv  32148  doch0  32218  doch1  32219  lcfl7lem  32359  mapdheq  32588  hdmap1eq  32662  hdmapval2lem  32694  hgmapvvlem3  32788
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 179  df-an 362
  Copyright terms: Public domain W3C validator