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

Theorem mpdan 668
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 22 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  mpan2  671  mpjaodan  784  mpd3an3  1325  eueq2  3277  csbiegf  3459  difsnb  4169  reusv3i  4654  fvtresfn  5951  fvmpt3  5953  ffvelrnd  6022  fnressn  6073  f1oiso2  6236  riota5f  6270  onsucuni  6647  seqomlem2  7116  oaordi  7195  nnaordi  7267  qsdisj  7388  dom2lem  7555  canth2g  7671  limenpsi  7692  php4  7704  onfin  7708  sucxpdom  7729  xpfi  7791  dmfi  7803  pwfilem  7814  pwfi  7815  fiin  7882  supiso  7933  ordiso2  7940  wemaplem2  7972  wdom2d  8006  infeq5  8054  cantnfp1lem3  8099  cantnflem1d  8107  cantnfp1lem3OLD  8125  cantnflem1dOLD  8130  r1val1  8204  rankwflemb  8211  onenon  8330  cardonle  8338  sdomsdomcardi  8352  acni  8426  cardaleph  8470  cdaen  8553  cdainf  8572  infcda1  8573  pwsdompw  8584  infdif  8589  cfval  8627  fin34  8770  fin1a2lem1  8780  fin1a2  8795  ttukeylem6  8894  sdomsdomcard  8935  canth3  8936  fpwwe2  9021  canthwelem  9028  gchcda1  9034  pwfseqlem4  9040  gchcdaidm  9046  gchxpidm  9047  tskwe2  9151  rankcf  9155  tskuni  9161  gruxp  9185  dmrecnq  9346  lterpq  9348  archnq  9358  reclem3pr  9427  reclem4pr  9428  0idsr  9474  lep1  10381  ledivp1  10447  supmul1  10508  suprzcl  10940  uz11  11104  zmin  11178  zbtwnre  11180  rpnnen1lem4  11211  rpnnen1lem5  11212  xnegid  11435  xleadd1a  11445  xlt2add  11452  xmullem  11456  xmulgt0  11475  xmulasslem3  11478  xlemul1a  11480  xadddilem  11486  xadddi  11487  xadddi2  11489  xrsupss  11500  xrinfmss  11501  supxrre  11519  infmxrre  11527  eluzfz2  11694  fzsuc  11727  fzsuc2  11737  fzp1disj  11738  fzneuz  11759  fllep1  11906  fraclt1  11907  fracle1  11908  fracge0  11909  flhalf  11930  ceige  11940  ceim1l  11942  fldiv  11955  modval  11966  suppssfz  12068  seqeq1  12078  expubnd  12194  iexpcyc  12240  faclbnd4lem3  12341  faclbnd4lem4  12342  swrdccat3blem  12683  cshwn  12731  shftfval  12866  shftcan1  12879  reval  12902  cjmulrcl  12940  addcj  12944  absval  13034  absneg  13073  abscj  13075  sqabsadd  13078  sqabssub  13079  leabs  13095  sqreulem  13155  lo1res  13345  o1of2  13398  o1rlimmul  13404  sumrb  13498  flo1  13629  trirecip  13637  efcan  13692  efi4p  13733  resin4p  13734  recos4p  13735  sincossq  13772  ruclem10  13833  iddvds  13858  1dvds  13859  2ebits  13956  1idssfct  14082  exprmfct  14110  eulerthlem2  14171  odzphi  14182  pcprendvds  14223  pcmpt  14270  vdwlem8  14365  0ram2  14398  pwsvscaval  14750  issect2  15010  homarel  15221  joinfval  15488  meetfval  15502  latjcom  15546  latmcom  15562  grprcan  15893  isgrpid2  15896  grpinvid  15911  mulgnn0z  15972  0subg  16031  divs0  16064  ghmker  16097  symginv  16232  symgfixfvh  16266  pmtrfrn  16289  odmulg2  16383  slwpgp  16439  pj1eq  16524  efgtf  16546  frgpinv  16588  frgpup2  16600  mulgnn0di  16640  cnaddablx  16677  cnaddabl  16678  zaddablx  16679  dprdfadd  16862  dprdfaddOLD  16869  dpjidcl  16909  dpjlid  16912  dpjidclOLD  16916  pgpfac1lem3  16930  srgen1zr  16983  rnglz  17036  rngrz  17037  1unit  17108  unitgrpid  17119  1rinv  17129  irredn0  17153  irredneg  17160  isdrng2  17206  abv0  17280  abv1z  17281  abvneg  17283  lsssn0  17394  lspsn0  17454  lsp0  17455  lmhmvsca  17491  lmhmrnlss  17496  lmhmkerlss  17497  lsppratlem5  17597  rsp1  17671  ringen1zr  17724  rlmassa  17774  asclpropd  17794  snifpsrbag  17814  psrvscaval  17844  psrdi  17860  psrdir  17861  mplsubglem  17892  mplsubglemOLD  17894  mplvscaval  17909  coe1sclmulfv  18123  ply1idvr1  18133  evl1var  18171  cnfldneg  18243  zringcyg  18308  zcyg  18313  chrid  18359  chrrhm  18363  ip0r  18467  ocvlss  18498  ocv1  18505  mamuvs1  18702  mamuvs2  18703  matecl  18722  matvscacell  18733  mat0scmat  18835  submaval0  18877  mdetrsca  18900  maduval  18935  minmar1val0  18944  pmatcollpw3fi1lem2  19083  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  chcoeffeqlem  19181  cayleyhamilton0  19185  cayleyhamiltonALT  19187  cctop  19301  cldval  19318  ntrfval  19319  clsfval  19320  cmclsopn  19357  opncldf3  19381  neifval  19394  lpfval  19433  cnrmnrm  19656  tx1cn  19873  tx2cn  19874  idqtop  19970  kqtopon  19991  kqid  19992  kqcld  19999  hmphen2  20063  filssufil  20176  ufileu  20183  alexsublem  20307  symgtgp  20363  ustuqtop4  20510  ustuqtop5  20511  cstucnd  20550  isxmet2d  20593  metustexhalfOLD  20829  metustexhalf  20830  nm0  20909  rlmnlm  20960  nmolb  20987  metdseq0  21121  iocopnst  21203  icccvx  21213  pi1xfrval  21317  clmvneg1  21354  ipcau2  21440  tchcphlem1  21441  tchcphlem2  21442  cmetcaulem  21490  ivthicc  21633  ovolicc2lem3  21693  ovolicc2lem4  21694  mbfmulc2lem  21817  i1fpos  21876  mbfi1fseqlem3  21887  mbfi1fseqlem4  21888  itg2ge0  21905  dvres2  22079  dvaddbr  22104  dvmulbr  22105  dvcobr  22112  c1lip1  22161  dvivth  22174  dvfsumlem4  22193  ftc1a  22201  ftc1lem6  22205  uc1pmon1p  22315  ig1pval2  22337  dgradd2  22427  dgrcolem2  22433  plydivlem4  22454  plydiveu  22456  elqaalem3  22479  qaa  22481  ulmdvlem1  22557  abelthlem6  22593  abelthlem7  22595  reeff1o  22604  coseq00topi  22656  tanabsge  22660  eflogeq  22742  logcnlem3  22781  atantan  23010  atanbnd  23013  cvxcl  23070  jensenlem2  23073  harmonicbnd4  23096  sgmnncl  23177  dchrptlem2  23296  1lgs  23368  lgs1  23369  dchrisumlem2  23431  dchrisum0lem2a  23458  selberg2lem  23491  pntrsumo1  23506  pntrsumbnd  23507  pntpbnd1  23527  pntlemr  23543  pntlemj  23544  ostthlem1  23568  padicabvf  23572  tglineeltr  23753  ttgval  23882  xmstrkgc  23893  cusgraexilem2  24171  cusgraexi  24172  cusgrasizeinds  24180  wwlksubclwwlk  24508  erclwwlkref  24517  erclwwlknref  24529  eupacl  24673  eupapf  24676  eupaseg  24677  frgrancvvdeqlemC  24744  frghash2spot  24768  isgrpoi  24904  grpoinvfval  24930  grpoinvid  24938  grpodivfval  24948  gxfval  24963  gxid  24979  issubgo  25009  cnaddablo  25056  ghomid  25071  rngolz  25107  rngorz  25108  rngosn6  25134  vcz  25167  vcoprne  25176  nvz0  25275  sspz  25352  lno0  25375  nmobndi  25394  ipasslem2  25451  shunssi  25990  ococin  26030  ssjo  26069  pjocini  26320  nlfnval  26504  lncnopbd  26660  riesz3i  26685  cnlnadjlem7  26696  pjclem4  26822  pj3si  26830  hstoc  26845  hstnmoc  26846  hstoh  26855  hst0  26856  mdsl2i  26945  chirredlem3  27015  chirredlem4  27016  dmdbr5ati  27045  rexunirn  27094  fcnvgreu  27214  xrpxdivcld  27327  omndmul2  27392  omndmul  27394  isarchi3  27421  orng0le1  27493  esumcst  27739  esumcvg  27760  sigaval  27778  measval  27837  eulerpartlemgvv  27983  probfinmeasb  28036  ballotlemfc0  28099  ballotlemfcc  28100  ballotlemsi  28121  ballotlemfrci  28134  signspval  28177  signlem0  28212  erdszelem7  28309  erdszelem8  28310  cvmliftlem10  28407  cvmliftlem13  28409  cvmlift2lem9  28424  cvmlift3lem6  28437  cvmlift3lem7  28438  cvmlift3lem9  28440  ghomgrpilem2  28529  prodrblem2  28668  dfrdg2  28833  dftrpred3g  28921  wfrlem5  28952  frrlem5  28996  bdayval  29013  ontopbas  29498  supaddc  29646  ismblfin  29660  cnambfre  29668  bddiblnc  29690  ftc1cnnc  29694  dvasin  29708  cldregopn  29754  islocfin  29796  tailfval  29821  filnetlem3  29829  filnetlem4  29830  ismtyres  29935  heiborlem8  29945  rngonegmn1l  29983  rngonegmn1r  29984  rngoneglmul  29985  rngonegrmul  29986  idlnegcl  30050  0idl  30053  0rngo  30055  keridl  30060  smprngopr  30080  mzpval  30296  mzpindd  30310  pellex  30403  2nn0ind  30513  jm2.26lem3  30575  pw2f1o2val  30613  wepwsolem  30619  fnwe2lem3  30630  lnmfg  30660  dgrsub2  30716  mpaaeu  30732  flcidc  30756  dvconstbi  30867  icccncfext  31254  itgsin0pilem1  31295  stoweidlem22  31350  stoweidlem32  31360  stoweidlem35  31363  stoweidlem36  31364  stoweidlem37  31365  stoweidlem43  31371  stoweidlem50  31378  wallispilem5  31397  stirlinglem2  31403  stirlinglem3  31404  stirlinglem4  31405  stirlinglem8  31409  stirlinglem11  31412  stirlinglem12  31413  stirlinglem14  31415  stirlinglem15  31416  fourierdlem49  31484  fourierdlem79  31514  usgrauvtxvd  31853  vdcusgra  31854  usgedgvadf1lem2  31909  usgedgvadf1ALTlem2  31912  isclintop  31987  clintopcllaw  31991  mgmcllaw  31995  assasslaw  31996  nzrneg1ne0  32059  coe1id  32083  bnj1006  33114  bnj1110  33135  bnj1253  33170  bnj1280  33173  bnj1463  33208  bnj1312  33211  lshpne0  33801  lkrval  33903  ldualvaddval  33946  ldualvsval  33953  opoc1  34017  pmap0  34579  pmap1N  34581  pexmidALTN  34792  cdleme31fv  35204  cdlemg27b  35510  erngdvlem4  35805  erng0g  35808  erngdvlem4-rN  35813  dvalveclem  35840  dvh0g  35926  dih0cnv  36098  dih1rn  36102  dih1cnv  36103  doch0  36173  doch1  36174  lcfl7lem  36314  mapdheq  36543  hdmap1eq  36617  hdmapval2lem  36649  hgmapvvlem3  36743
  Copyright terms: Public domain W3C validator