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  1316  eueq2  3238  csbiegf  3418  difsnb  4122  reusv3i  4606  fvtresfn  5883  fvmpt3  5885  ffvelrnd  5952  fnressn  6002  f1oiso2  6151  riota5f  6185  onsucuni  6548  seqomlem2  7015  oaordi  7094  nnaordi  7166  qsdisj  7286  dom2lem  7458  canth2g  7574  limenpsi  7595  php4  7607  onfin  7611  sucxpdom  7632  xpfi  7693  dmfi  7704  pwfilem  7715  pwfi  7716  fiin  7782  supiso  7832  ordiso2  7839  wemaplem2  7871  wdom2d  7905  infeq5  7953  cantnfp1lem3  7998  cantnflem1d  8006  cantnfp1lem3OLD  8024  cantnflem1dOLD  8029  r1val1  8103  rankwflemb  8110  onenon  8229  cardonle  8237  sdomsdomcardi  8251  acni  8325  cardaleph  8369  cdaen  8452  cdainf  8471  infcda1  8472  pwsdompw  8483  infdif  8488  cfval  8526  fin34  8669  fin1a2lem1  8679  fin1a2  8694  ttukeylem6  8793  sdomsdomcard  8834  canth3  8835  fpwwe2  8920  canthwelem  8927  gchcda1  8933  pwfseqlem4  8939  gchcdaidm  8945  gchxpidm  8946  tskwe2  9050  rankcf  9054  tskuni  9060  gruxp  9084  dmrecnq  9247  lterpq  9249  archnq  9259  reclem3pr  9328  reclem4pr  9329  0idsr  9374  lep1  10278  ledivp1  10344  supmul1  10405  suprzcl  10831  uz11  10993  zmin  11059  zbtwnre  11061  rpnnen1lem4  11092  rpnnen1lem5  11093  xnegid  11316  xleadd1a  11326  xlt2add  11333  xmullem  11337  xmulgt0  11356  xmulasslem3  11359  xlemul1a  11361  xadddilem  11367  xadddi  11368  xadddi2  11370  xrsupss  11381  xrinfmss  11382  supxrre  11400  infmxrre  11408  eluzfz2  11575  fzsuc  11618  fzsuc2  11630  fzp1disj  11631  fzneuz  11657  fllep1  11767  fraclt1  11768  fracle1  11769  fracge0  11770  flhalf  11790  ceige  11800  ceim1l  11802  fldiv  11815  modval  11826  seqeq1  11925  expubnd  12040  iexpcyc  12086  faclbnd4lem3  12187  faclbnd4lem4  12188  swrdccat3blem  12503  cshwn  12551  shftfval  12676  shftcan1  12689  reval  12712  cjmulrcl  12750  addcj  12754  absval  12844  absneg  12883  abscj  12885  sqabsadd  12888  sqabssub  12889  leabs  12905  sqreulem  12964  lo1res  13154  o1of2  13207  o1rlimmul  13213  sumrb  13307  flo1  13434  trirecip  13442  efcan  13497  efi4p  13538  resin4p  13539  recos4p  13540  sincossq  13577  ruclem10  13638  iddvds  13663  1dvds  13664  2ebits  13760  1idssfct  13886  exprmfct  13913  eulerthlem2  13974  odzphi  13985  pcprendvds  14024  pcmpt  14071  vdwlem8  14166  0ram2  14199  pwsvscaval  14551  issect2  14811  homarel  15022  joinfval  15289  meetfval  15303  latjcom  15347  latmcom  15363  grprcan  15689  isgrpid2  15692  grpinvid  15707  mulgnn0z  15765  0subg  15824  divs0  15857  ghmker  15890  symginv  16025  symgfixfvh  16059  pmtrfrn  16082  odmulg2  16176  slwpgp  16232  pj1eq  16317  efgtf  16339  frgpinv  16381  frgpup2  16393  mulgnn0di  16433  cnaddablx  16468  cnaddabl  16469  zaddablx  16470  dprdfadd  16631  dprdfaddOLD  16638  dpjidcl  16678  dpjlid  16681  dpjidclOLD  16685  pgpfac1lem3  16699  rnglz  16803  rngrz  16804  1unit  16872  unitgrpid  16883  1rinv  16893  irredn0  16917  irredneg  16924  isdrng2  16964  abv0  17038  abv1z  17039  abvneg  17041  lsssn0  17151  lspsn0  17211  lsp0  17212  lmhmvsca  17248  lmhmrnlss  17253  lmhmkerlss  17254  lsppratlem5  17354  rsp1  17428  rlmassa  17519  asclpropd  17538  snifpsrbag  17555  psrvscaval  17585  psrdi  17601  psrdir  17602  mplsubglem  17633  mplsubglemOLD  17635  mplvscaval  17650  coe1sclmulfv  17859  evl1var  17894  cnfldneg  17966  zringcyg  18031  zcyg  18036  chrid  18082  chrrhm  18086  ip0r  18190  ocvlss  18221  ocv1  18228  mamuvs1  18433  mamuvs2  18434  matecl  18450  submaval0  18517  mdetrsca  18540  maduval  18575  minmar1val0  18584  cctop  18741  cldval  18758  ntrfval  18759  clsfval  18760  cmclsopn  18797  opncldf3  18821  neifval  18834  lpfval  18873  cnrmnrm  19096  tx1cn  19313  tx2cn  19314  idqtop  19410  kqtopon  19431  kqid  19432  kqcld  19439  hmphen2  19503  filssufil  19616  ufileu  19623  alexsublem  19747  symgtgp  19803  ustuqtop4  19950  ustuqtop5  19951  cstucnd  19990  isxmet2d  20033  metustexhalfOLD  20269  metustexhalf  20270  nm0  20349  rlmnlm  20400  nmolb  20427  metdseq0  20561  iocopnst  20643  icccvx  20653  pi1xfrval  20757  clmvneg1  20794  ipcau2  20880  tchcphlem1  20881  tchcphlem2  20882  cmetcaulem  20930  ivthicc  21073  ovolicc2lem3  21133  ovolicc2lem4  21134  mbfmulc2lem  21257  i1fpos  21316  mbfi1fseqlem3  21327  mbfi1fseqlem4  21328  itg2ge0  21345  dvres2  21519  dvaddbr  21544  dvmulbr  21545  dvcobr  21552  c1lip1  21601  dvivth  21614  dvfsumlem4  21633  ftc1a  21641  ftc1lem6  21645  uc1pmon1p  21755  ig1pval2  21777  dgradd2  21867  dgrcolem2  21873  plydivlem4  21894  plydiveu  21896  elqaalem3  21919  qaa  21921  ulmdvlem1  21997  abelthlem6  22033  abelthlem7  22035  reeff1o  22044  coseq00topi  22096  tanabsge  22100  eflogeq  22182  logcnlem3  22221  atantan  22450  atanbnd  22453  cvxcl  22510  jensenlem2  22513  harmonicbnd4  22536  sgmnncl  22617  dchrptlem2  22736  1lgs  22808  lgs1  22809  dchrisumlem2  22871  dchrisum0lem2a  22898  selberg2lem  22931  pntrsumo1  22946  pntrsumbnd  22947  pntpbnd1  22967  pntlemr  22983  pntlemj  22984  ostthlem1  23008  padicabvf  23012  tglineeltr  23175  ttgval  23272  xmstrkgc  23283  cusgraexilem2  23526  cusgraexi  23527  cusgrasizeinds  23535  eupacl  23741  eupapf  23744  eupaseg  23745  isgrpoi  23836  grpoinvfval  23862  grpoinvid  23870  grpodivfval  23880  gxfval  23895  gxid  23911  issubgo  23941  cnaddablo  23988  ghomid  24003  rngolz  24039  rngorz  24040  rngosn6  24066  vcz  24099  vcoprne  24108  nvz0  24207  sspz  24284  lno0  24307  nmobndi  24326  ipasslem2  24383  shunssi  24922  ococin  24962  ssjo  25001  pjocini  25252  nlfnval  25436  lncnopbd  25592  riesz3i  25617  cnlnadjlem7  25628  pjclem4  25754  pj3si  25762  hstoc  25777  hstnmoc  25778  hstoh  25787  hst0  25788  mdsl2i  25877  chirredlem3  25947  chirredlem4  25948  dmdbr5ati  25977  rexunirn  26026  fcnvgreu  26141  xrpxdivcld  26254  omndmul2  26319  omndmul  26321  isarchi3  26348  orng0le1  26424  esumcst  26658  esumcvg  26679  sigaval  26697  measval  26756  eulerpartlemgvv  26902  probfinmeasb  26955  ballotlemfc0  27018  ballotlemfcc  27019  ballotlemsi  27040  ballotlemfrci  27053  signspval  27096  signlem0  27131  erdszelem7  27228  erdszelem8  27229  cvmliftlem10  27326  cvmliftlem13  27328  cvmlift2lem9  27343  cvmlift3lem6  27356  cvmlift3lem7  27357  cvmlift3lem9  27359  ghomgrpilem2  27448  prodrblem2  27587  dfrdg2  27752  dftrpred3g  27840  wfrlem5  27871  frrlem5  27915  bdayval  27932  ontopbas  28417  supaddc  28564  ismblfin  28579  cnambfre  28587  bddiblnc  28609  ftc1cnnc  28613  dvasin  28627  cldregopn  28673  islocfin  28715  tailfval  28740  filnetlem3  28748  filnetlem4  28749  ismtyres  28854  heiborlem8  28864  rngonegmn1l  28902  rngonegmn1r  28903  rngoneglmul  28904  rngonegrmul  28905  idlnegcl  28969  0idl  28972  0rngo  28974  keridl  28979  smprngopr  28999  mzpval  29215  mzpindd  29229  pellex  29323  2nn0ind  29433  jm2.26lem3  29497  pw2f1o2val  29535  wepwsolem  29541  fnwe2lem3  29552  lnmfg  29582  dgrsub2  29638  mpaaeu  29654  flcidc  29678  dvconstbi  29755  itgsin0pilem1  29937  stoweidlem22  29964  stoweidlem32  29974  stoweidlem35  29977  stoweidlem36  29978  stoweidlem37  29979  stoweidlem43  29985  stoweidlem50  29992  wallispilem5  30011  stirlinglem2  30017  stirlinglem3  30018  stirlinglem4  30019  stirlinglem8  30023  stirlinglem11  30026  stirlinglem12  30027  stirlinglem14  30029  stirlinglem15  30030  wwlksubclwwlk  30613  erclwwlkref  30630  erclwwlknref  30646  usgrauvtxvd  30677  vdcusgra  30678  frgrancvvdeqlemC  30779  frghash2spot  30803  nzrneg1ne0  30927  suppssfz  30933  ply1idvr1  30979  coe1id  30986  matvscacell  31020  m2cnstpminv  31226  pmatcollpw3fi1lem2  31259  chfacfscmulgsum  31331  chfacfpmmulgsum  31335  cpmadumatpolylem2  31353  chcoeffeqlem  31357  cayleyhamilton0  31361  cayleyhamiltonALT  31363  bnj1006  32269  bnj1110  32290  bnj1253  32325  bnj1280  32328  bnj1463  32363  bnj1312  32366  lshpne0  32954  lkrval  33056  ldualvaddval  33099  ldualvsval  33106  opoc1  33170  pmap0  33732  pmap1N  33734  pexmidALTN  33945  cdleme31fv  34357  cdlemg27b  34663  erngdvlem4  34958  erng0g  34961  erngdvlem4-rN  34966  dvalveclem  34993  dvh0g  35079  dih0cnv  35251  dih1rn  35255  dih1cnv  35256  doch0  35326  doch1  35327  lcfl7lem  35467  mapdheq  35696  hdmap1eq  35770  hdmapval2lem  35802  hgmapvvlem3  35896
  Copyright terms: Public domain W3C validator