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 22 . 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  3182  csbiegf  3357  difsnb  4080  reusv3i  4569  fvtresfn  5905  fvmpt3  5907  ffvelrnd  5977  fnressn  6030  fsnex  6135  f1oiso2  6197  riota5f  6230  onsucuni  6608  wfrlem5  6990  seqomlem2  7118  oaordi  7197  nnaordi  7269  qsdisj  7390  dom2lem  7558  canth2g  7674  limenpsi  7695  php4  7707  onfin  7711  sucxpdom  7729  xpfi  7790  dmfi  7802  pwfilem  7816  pwfi  7817  fiin  7884  supiso  7939  ordiso2  7978  wdom2d  8043  infeq5  8090  cantnfp1lem3  8132  cantnflem1d  8140  rankwflemb  8211  onenon  8330  cardonle  8338  sdomsdomcardi  8352  acni  8422  cardaleph  8466  cdaen  8549  cdainf  8568  infcda1  8569  pwsdompw  8580  infdif  8585  cfval  8623  fin34  8766  fin1a2lem1  8776  fin1a2  8791  ttukeylem6  8890  sdomsdomcard  8931  canth3  8932  fpwwe2  9014  canthwelem  9021  gchcda1  9027  pwfseqlem4  9033  gchcdaidm  9039  gchxpidm  9040  tskwe2  9144  rankcf  9148  tskuni  9154  gruxp  9178  dmrecnq  9339  lterpq  9341  archnq  9351  reclem3pr  9420  reclem4pr  9421  0idsr  9467  lep1  10390  ledivp1  10454  negfi  10500  supaddc  10520  supmul1  10522  suprzcl  10961  uz11  11127  zmin  11206  zbtwnre  11208  rpnnen1lem4  11239  rpnnen1lem5  11240  xnegid  11475  xrsupss  11540  xrinfmss  11541  supxrre  11559  infxrre  11568  infmxrreOLD  11572  eluzfz2  11753  fzsuc  11789  fzsuc2  11799  fzp1disj  11800  fzneuz  11821  fllep1  11982  fraclt1  11983  fracle1  11984  fracge0  11985  flhalf  12007  ceige  12017  ceim1l  12019  fldiv  12032  modval  12043  suppssfz  12151  seqeq1  12161  expubnd  12278  iexpcyc  12324  faclbnd4lem3  12425  faclbnd4lem4  12426  swrdid  12725  swrdccat3blem  12792  cshwn  12840  trclexlem  12997  shftfval  13072  shftcan1  13085  reval  13108  cjmulrcl  13146  addcj  13150  absval  13240  absneg  13279  abscj  13281  sqabsadd  13284  sqabssub  13285  leabs  13301  sqreulem  13361  lo1res  13561  o1of2  13614  o1rlimmul  13620  sumrb  13717  flo1  13850  trirecip  13859  prodrblem2  13923  efcan  14088  efi4p  14129  resin4p  14130  recos4p  14131  sincossq  14168  ruclem10  14229  iddvds  14254  1dvds  14255  2ebits  14359  lcmftp  14547  1idssfct  14568  exprmfct  14586  coprmgcdb  14592  eulerthlem2  14668  odzphi  14679  odzphiOLD  14685  pcprendvds  14728  pcmpt  14775  vdwlem8  14876  0ram2  14917  prmgaplem7  14965  pwsvscaval  15331  issect2  15597  2initoinv  15843  initoeu1  15844  initoeu2lem1  15847  initoeu2  15849  2termoinv  15850  termoeu1  15851  homarel  15869  joinfval  16185  meetfval  16199  latjcom  16243  latmcom  16259  sgrp2nmndlem5  16601  grprcan  16637  isgrpid2  16640  grpinvid  16655  mulgnn0z  16716  0subg  16780  qus0  16813  ghmker  16846  symginv  16981  pmtrfrn  17037  odmulg2  17144  slwpgp  17203  pj1eq  17288  efgtf  17310  frgpinv  17352  frgpup2  17364  mulgnn0di  17404  cnaddablx  17444  cnaddabl  17445  zaddablx  17446  dprdfadd  17591  dpjidcl  17629  dpjlid  17632  pgpfac1lem3  17648  srgen1zr  17701  ringlz  17755  ringrz  17756  1unit  17824  unitgrpid  17835  1rinv  17845  irredn0  17869  irredneg  17876  isdrng2  17923  abv0  17997  abv1z  17998  abvneg  18000  lsssn0  18109  lspsn0  18169  lsp0  18170  lmhmvsca  18206  lmhmrnlss  18211  lmhmkerlss  18212  lsppratlem5  18312  rsp1  18386  ringen1zr  18439  rlmassa  18488  asclpropd  18508  snifpsrbag  18528  psrvscaval  18554  psrdi  18568  psrdir  18569  mplsubglem  18596  mplvscaval  18610  coe1sclmulfv  18814  ply1idvr1  18824  evl1var  18862  cnfldneg  18932  zringcyg  18997  chrid  19035  chrrhm  19039  ip0r  19141  ocvlss  19172  ocv1  19179  mamuvs1  19367  mamuvs2  19368  matecl  19387  matvscacell  19398  mat0scmat  19500  submaval0  19542  mdetrsca  19565  maduval  19600  minmar1val0  19609  pmatcollpw3fi1lem2  19748  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  chcoeffeqlem  19846  cayleyhamilton0  19850  cayleyhamiltonALT  19852  cctop  19958  cldval  19975  ntrfval  19976  clsfval  19977  cmclsopn  20014  opncldf3  20039  neifval  20052  lpfval  20091  cnrmnrm  20314  islocfin  20469  tx1cn  20561  tx2cn  20562  idqtop  20658  kqtopon  20679  kqid  20680  kqcld  20687  hmphen2  20751  filssufil  20864  ufileu  20871  alexsublem  20996  symgtgp  21053  ustuqtop4  21196  ustuqtop5  21197  cstucnd  21236  metustexhalf  21508  nm0  21577  rlmnlm  21628  nmolb  21659  nmolbOLD  21678  metdseq0  21808  metdseq0OLD  21823  iocopnst  21905  pi1xfrval  22022  clmvneg1  22059  ipcau2  22145  tchcphlem1  22146  tchcphlem2  22147  cmetcaulem  22195  ovolicc2lem3  22409  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  mbfmulc2lem  22540  i1fpos  22601  mbfi1fseqlem3  22612  mbfi1fseqlem4  22613  itg2ge0  22630  dvres2  22804  dvaddbr  22829  dvmulbr  22830  dvcobr  22837  dvfsumlem4  22918  ftc1a  22926  ftc1lem6  22930  uc1pmon1p  23039  ig1pval2  23062  ig1pval2OLD  23068  dgradd2  23159  dgrcolem2  23165  plydivlem4  23186  plydiveu  23188  elqaalem3  23211  elqaalem3OLD  23214  qaa  23216  ulmdvlem1  23292  abelthlem6  23328  abelthlem7  23330  eflogeq  23488  jensenlem2  23850  harmonicbnd4  23873  sgmnncl  24011  dchrptlem2  24130  1lgs  24202  lgs1  24203  dchrisumlem2  24265  dchrisum0lem2a  24292  selberg2lem  24325  pntrsumo1  24340  pntrsumbnd  24341  pntpbnd1  24361  pntlemr  24377  pntlemj  24378  padicabvf  24406  istrkg3ld  24446  tglineeltr  24613  cusgraexilem2  25132  cusgraexi  25133  cusgrasizeinds  25141  wwlksubclwwlk  25469  erclwwlkref  25478  erclwwlknref  25490  eupacl  25634  eupapf  25637  eupaseg  25638  frgrancvvdeqlemC  25704  frghash2spot  25728  isgrpoi  25863  grpoinvfval  25889  grpoinvid  25897  grpodivfval  25907  gxfval  25922  gxid  25938  issubgo  25968  cnaddablo  26015  ghomidOLD  26030  rngolz  26066  rngorz  26067  rngosn6  26093  vcz  26126  vcoprne  26135  nvz0  26234  sspz  26311  lno0  26334  nmobndi  26353  ipasslem2  26410  shunssi  26958  ococin  26998  ssjo  27037  pjocini  27288  nlfnval  27471  lncnopbd  27627  riesz3i  27652  cnlnadjlem7  27663  pjclem4  27789  pj3si  27797  hstoc  27812  hstnmoc  27813  hstoh  27822  hst0  27823  mdsl2i  27912  chirredlem3  27982  chirredlem4  27983  dmdbr5ati  28012  rexunirn  28064  fcnvgreu  28216  infxrge0glb  28293  infxrge0glbOLD  28294  2sqcoprm  28354  omndmul2  28421  omndmul  28423  isarchi3  28450  orng0le1  28522  esumcvg  28854  esumcvgre  28859  sigaval  28879  unelldsys  28927  fiunelros  28943  measval  28967  pmeasmono  29104  eulerpartlemgvv  29156  probfinmeasb  29209  ballotlemfc0  29272  ballotlemfcc  29273  ballotlemsi  29294  ballotlemfrci  29307  ballotlemsiOLD  29332  ballotlemfrciOLD  29345  sgnneg  29358  signlem0  29423  bnj1006  29717  bnj1110  29738  bnj1253  29773  bnj1280  29776  bnj1463  29811  bnj1312  29814  erdszelem7  29867  erdszelem8  29868  cvmliftlem10  29964  cvmliftlem13  29966  cvmlift2lem9  29981  cvmlift3lem6  29994  cvmlift3lem7  29995  cvmlift3lem9  29997  ghomgrpilem2  30251  dfrdg2  30388  dftrpred3g  30420  frrlem5  30464  bdayval  30481  cldregopn  30931  tailfval  30972  filnetlem3  30980  filnetlem4  30981  ontopbas  31032  f1omptsnlem  31645  icoreunrn  31669  relowlpssretop  31674  wl-sbal2  31801  poimirlem1  31848  poimirlem2  31849  poimirlem4  31851  poimirlem6  31853  poimirlem7  31854  poimirlem11  31858  poimirlem12  31859  poimirlem17  31864  poimirlem20  31867  poimirlem22  31869  poimirlem23  31870  poimirlem28  31875  poimir  31880  ismblfin  31888  cnambfre  31896  bddiblnc  31919  ftc1cnnc  31923  dvasin  31935  ismtyres  32047  heiborlem8  32057  rngonegmn1l  32095  rngonegmn1r  32096  rngoneglmul  32097  rngonegrmul  32098  idlnegcl  32162  0idl  32165  0rngo  32167  keridl  32172  smprngopr  32192  lshpne0  32464  lkrval  32566  ldualvaddval  32609  ldualvsval  32616  opoc1  32680  pmap0  33242  pmap1N  33244  pexmidALTN  33455  cdleme31fv  33869  cdlemg27b  34175  erngdvlem4  34470  erng0g  34473  erngdvlem4-rN  34478  dvalveclem  34505  dvh0g  34591  dih0cnv  34763  dih1rn  34767  dih1cnv  34768  doch0  34838  doch1  34839  lcfl7lem  34979  mapdheq  35208  hdmap1eq  35282  hdmapval2lem  35314  hgmapvvlem3  35408  mzpval  35486  mzpindd  35500  pellex  35592  2nn0ind  35706  jm2.26lem3  35769  pw2f1o2val  35807  wepwsolem  35813  fnwe2lem3  35823  lnmfg  35853  dgrsub2  35907  mpaaeu  35929  flcidc  35953  rtrclexlem  36136  cnvrcl0  36145  suprleubrd  36522  suprlubrd  36526  imo72b2  36532  dvconstbi  36596  bcc0  36602  binomcxplemnotnn0  36618  nnfoctb  37299  sumnnodd  37593  icccncfext  37648  itgsin0pilem1  37709  stoweidlem22  37765  stoweidlem32  37776  stoweidlem35  37779  stoweidlem36  37780  stoweidlem37  37781  stoweidlem43  37787  stoweidlem50  37794  wallispilem5  37814  stirlinglem2  37820  stirlinglem3  37821  stirlinglem4  37822  stirlinglem8  37826  stirlinglem11  37829  stirlinglem12  37830  stirlinglem14  37832  stirlinglem15  37833  fourierdlem11  37863  fourierdlem20  37872  fourierdlem21  37873  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem49  37902  fourierdlem64  37917  fourierdlem71  37924  fourierdlem79  37932  fourierdlem90  37943  fourierdlem91  37944  fourierswlem  37977  etransclem17  37999  etransclem38  38020  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  bgoldbtbnd  38717  pfxid  38746  pfx2  38766  structiedg0val  38898  incistruhgr  38945  subgrprop3  39085  subgruhgredgd  39093  usgrexi  39234  cusgrexi  39235  cusgrsizeinds  39241  usgrauvtxvd  39263  vdcusgra  39264  usgedgvadf1lem2  39317  usgedgvadf1ALTlem2  39320  isclintop  39434  clintopcllaw  39438  nzrneg1ne0  39460  rnglz  39475  c0snmgmhm  39505  zrrnghm  39508  lidldomn1  39512  uzlidlring  39520  2zrngnmlid  39540  cznrng  39548  zrinitorngc  39593  zrtermorngc  39594  zrtermoringc  39663  coe1id  39769  blenre  39978  blennn  39979
  Copyright terms: Public domain W3C validator