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

Theorem mpdan 666
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 659 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  mpan2  669  mpjaodan  784  mpd3an3  1323  eueq2  3198  csbiegf  3372  difsnb  4086  reusv3i  4572  fvtresfn  5858  fvmpt3  5860  ffvelrnd  5934  fnressn  5985  f1oiso2  6149  riota5f  6182  onsucuni  6562  seqomlem2  7034  oaordi  7113  nnaordi  7185  qsdisj  7306  dom2lem  7474  canth2g  7590  limenpsi  7611  php4  7623  onfin  7627  sucxpdom  7645  xpfi  7706  dmfi  7718  pwfilem  7729  pwfi  7730  fiin  7797  supiso  7848  ordiso2  7855  wdom2d  7921  infeq5  7968  cantnfp1lem3  8012  cantnflem1d  8020  cantnfp1lem3OLD  8038  cantnflem1dOLD  8043  rankwflemb  8124  onenon  8243  cardonle  8251  sdomsdomcardi  8265  acni  8339  cardaleph  8383  cdaen  8466  cdainf  8485  infcda1  8486  pwsdompw  8497  infdif  8502  cfval  8540  fin34  8683  fin1a2lem1  8693  fin1a2  8708  ttukeylem6  8807  sdomsdomcard  8848  canth3  8849  fpwwe2  8932  canthwelem  8939  gchcda1  8945  pwfseqlem4  8951  gchcdaidm  8957  gchxpidm  8958  tskwe2  9062  rankcf  9066  tskuni  9072  gruxp  9096  dmrecnq  9257  lterpq  9259  archnq  9269  reclem3pr  9338  reclem4pr  9339  0idsr  9385  lep1  10298  ledivp1  10363  supmul1  10424  suprzcl  10859  uz11  11023  zmin  11097  zbtwnre  11099  rpnnen1lem4  11130  rpnnen1lem5  11131  xnegid  11356  xrsupss  11421  xrinfmss  11422  supxrre  11440  infmxrre  11448  eluzfz2  11615  fzsuc  11649  fzsuc2  11659  fzp1disj  11660  fzneuz  11681  fllep1  11837  fraclt1  11838  fracle1  11839  fracge0  11840  flhalf  11862  ceige  11872  ceim1l  11874  fldiv  11887  modval  11898  suppssfz  12003  seqeq1  12013  expubnd  12129  iexpcyc  12175  faclbnd4lem3  12275  faclbnd4lem4  12276  swrdid  12564  swrdccat3blem  12631  cshwn  12679  trclexlem  12832  shftfval  12905  shftcan1  12918  reval  12941  cjmulrcl  12979  addcj  12983  absval  13073  absneg  13112  abscj  13114  sqabsadd  13117  sqabssub  13118  leabs  13134  sqreulem  13194  lo1res  13384  o1of2  13437  o1rlimmul  13443  sumrb  13537  flo1  13668  trirecip  13676  prodrblem2  13740  efcan  13833  efi4p  13874  resin4p  13875  recos4p  13876  sincossq  13913  ruclem10  13974  iddvds  13999  1dvds  14000  2ebits  14099  1idssfct  14225  exprmfct  14253  eulerthlem2  14314  odzphi  14325  pcprendvds  14366  pcmpt  14413  vdwlem8  14508  0ram2  14541  pwsvscaval  14902  issect2  15160  2initoinv  15406  initoeu1  15407  initoeu2lem1  15410  initoeu2  15412  2termoinv  15413  termoeu1  15414  homarel  15432  joinfval  15748  meetfval  15762  latjcom  15806  latmcom  15822  sgrp2nmndlem5  16164  grprcan  16200  isgrpid2  16203  grpinvid  16218  mulgnn0z  16279  0subg  16343  qus0  16376  ghmker  16409  symginv  16544  pmtrfrn  16600  odmulg2  16694  slwpgp  16750  pj1eq  16835  efgtf  16857  frgpinv  16899  frgpup2  16911  mulgnn0di  16951  cnaddablx  16991  cnaddabl  16992  zaddablx  16993  dprdfadd  17173  dprdfaddOLD  17180  dpjidcl  17220  dpjlid  17223  dpjidclOLD  17227  pgpfac1lem3  17241  srgen1zr  17294  ringlz  17348  ringrz  17349  1unit  17420  unitgrpid  17431  1rinv  17441  irredn0  17465  irredneg  17472  isdrng2  17519  abv0  17593  abv1z  17594  abvneg  17596  lsssn0  17707  lspsn0  17767  lsp0  17768  lmhmvsca  17804  lmhmrnlss  17809  lmhmkerlss  17810  lsppratlem5  17910  rsp1  17985  ringen1zr  18038  rlmassa  18088  asclpropd  18108  snifpsrbag  18128  psrvscaval  18158  psrdi  18174  psrdir  18175  mplsubglem  18206  mplsubglemOLD  18208  mplvscaval  18223  coe1sclmulfv  18437  ply1idvr1  18447  evl1var  18485  cnfldneg  18557  zringcyg  18619  chrid  18657  chrrhm  18661  ip0r  18763  ocvlss  18794  ocv1  18801  mamuvs1  18992  mamuvs2  18993  matecl  19012  matvscacell  19023  mat0scmat  19125  submaval0  19167  mdetrsca  19190  maduval  19225  minmar1val0  19234  pmatcollpw3fi1lem2  19373  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  chcoeffeqlem  19471  cayleyhamilton0  19475  cayleyhamiltonALT  19477  cctop  19592  cldval  19609  ntrfval  19610  clsfval  19611  cmclsopn  19648  opncldf3  19673  neifval  19686  lpfval  19725  cnrmnrm  19948  islocfin  20103  tx1cn  20195  tx2cn  20196  idqtop  20292  kqtopon  20313  kqid  20314  kqcld  20321  hmphen2  20385  filssufil  20498  ufileu  20505  alexsublem  20629  symgtgp  20685  ustuqtop4  20832  ustuqtop5  20833  cstucnd  20872  metustexhalfOLD  21151  metustexhalf  21152  nm0  21231  rlmnlm  21282  nmolb  21309  metdseq0  21443  iocopnst  21525  pi1xfrval  21639  clmvneg1  21676  ipcau2  21762  tchcphlem1  21763  tchcphlem2  21764  cmetcaulem  21812  ovolicc2lem3  22015  ovolicc2lem4  22016  mbfmulc2lem  22139  i1fpos  22198  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  itg2ge0  22227  dvres2  22401  dvaddbr  22426  dvmulbr  22427  dvcobr  22434  dvfsumlem4  22515  ftc1a  22523  ftc1lem6  22527  uc1pmon1p  22637  ig1pval2  22659  dgradd2  22750  dgrcolem2  22756  plydivlem4  22777  plydiveu  22779  elqaalem3  22802  qaa  22804  ulmdvlem1  22880  abelthlem6  22916  abelthlem7  22918  eflogeq  23074  jensenlem2  23434  harmonicbnd4  23457  sgmnncl  23538  dchrptlem2  23657  1lgs  23729  lgs1  23730  dchrisumlem2  23792  dchrisum0lem2a  23819  selberg2lem  23852  pntrsumo1  23867  pntrsumbnd  23868  pntpbnd1  23888  pntlemr  23904  pntlemj  23905  padicabvf  23933  tglineeltr  24131  cusgraexilem2  24588  cusgraexi  24589  cusgrasizeinds  24597  wwlksubclwwlk  24925  erclwwlkref  24934  erclwwlknref  24946  eupacl  25090  eupapf  25093  eupaseg  25094  frgrancvvdeqlemC  25160  frghash2spot  25184  isgrpoi  25317  grpoinvfval  25343  grpoinvid  25351  grpodivfval  25361  gxfval  25376  gxid  25392  issubgo  25422  cnaddablo  25469  ghomidOLD  25484  rngolz  25520  rngorz  25521  rngosn6  25547  vcz  25580  vcoprne  25589  nvz0  25688  sspz  25765  lno0  25788  nmobndi  25807  ipasslem2  25864  shunssi  26403  ococin  26443  ssjo  26482  pjocini  26733  nlfnval  26916  lncnopbd  27072  riesz3i  27097  cnlnadjlem7  27108  pjclem4  27234  pj3si  27242  hstoc  27257  hstnmoc  27258  hstoh  27267  hst0  27268  mdsl2i  27357  chirredlem3  27427  chirredlem4  27428  dmdbr5ati  27457  rexunirn  27507  fcnvgreu  27660  2sqcoprm  27788  omndmul2  27855  omndmul  27857  isarchi3  27884  orng0le1  27956  esumcvg  28234  esumcvgre  28239  sigaval  28259  measval  28325  eulerpartlemgvv  28498  probfinmeasb  28551  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemsi  28636  ballotlemfrci  28649  sgnneg  28662  signlem0  28727  erdszelem7  28830  erdszelem8  28831  cvmliftlem10  28928  cvmliftlem13  28930  cvmlift2lem9  28945  cvmlift3lem6  28958  cvmlift3lem7  28959  cvmlift3lem9  28961  ghomgrpilem2  29215  dfrdg2  29393  dftrpred3g  29481  wfrlem5  29512  frrlem5  29556  bdayval  29573  ontopbas  30046  wl-sbal2  30179  supaddc  30206  ismblfin  30220  cnambfre  30228  bddiblnc  30251  ftc1cnnc  30255  dvasin  30269  cldregopn  30315  tailfval  30356  filnetlem3  30364  filnetlem4  30365  ismtyres  30470  heiborlem8  30480  rngonegmn1l  30518  rngonegmn1r  30519  rngoneglmul  30520  rngonegrmul  30521  idlnegcl  30585  0idl  30588  0rngo  30590  keridl  30595  smprngopr  30615  mzpval  30830  mzpindd  30844  pellex  30936  2nn0ind  31046  jm2.26lem3  31109  pw2f1o2val  31147  wepwsolem  31153  fnwe2lem3  31164  lnmfg  31194  dgrsub2  31252  mpaaeu  31267  flcidc  31291  dvconstbi  31407  bcc0  31413  binomcxplemnotnn0  31429  sumnnodd  31802  icccncfext  31856  itgsin0pilem1  31914  stoweidlem22  31970  stoweidlem32  31980  stoweidlem35  31983  stoweidlem36  31984  stoweidlem37  31985  stoweidlem43  31991  stoweidlem50  31998  wallispilem5  32017  stirlinglem2  32023  stirlinglem3  32024  stirlinglem4  32025  stirlinglem8  32029  stirlinglem11  32032  stirlinglem12  32033  stirlinglem14  32035  stirlinglem15  32036  fourierdlem11  32066  fourierdlem20  32075  fourierdlem21  32076  fourierdlem41  32096  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem64  32119  fourierdlem71  32126  fourierdlem79  32134  fourierdlem90  32145  fourierdlem91  32146  fourierswlem  32179  etransclem17  32200  etransclem38  32221  pfxid  32567  pfx2  32587  usgrauvtxvd  32676  vdcusgra  32677  usgedgvadf1lem2  32732  usgedgvadf1ALTlem2  32735  isclintop  32849  clintopcllaw  32853  nzrneg1ne0  32875  rnglz  32890  c0snmgmhm  32920  zrrnghm  32923  lidldomn1  32927  uzlidlring  32935  2zrngnmlid  32955  cznrng  32963  zrinitorngc  33008  zrtermorngc  33009  zrtermoringc  33078  coe1id  33184  blenre  33395  blennn  33396  bnj1006  34364  bnj1110  34385  bnj1253  34420  bnj1280  34423  bnj1463  34458  bnj1312  34461  lshpne0  35124  lkrval  35226  ldualvaddval  35269  ldualvsval  35276  opoc1  35340  pmap0  35902  pmap1N  35904  pexmidALTN  36115  cdleme31fv  36529  cdlemg27b  36835  erngdvlem4  37130  erng0g  37133  erngdvlem4-rN  37138  dvalveclem  37165  dvh0g  37251  dih0cnv  37423  dih1rn  37427  dih1cnv  37428  doch0  37498  doch1  37499  lcfl7lem  37639  mapdheq  37868  hdmap1eq  37942  hdmapval2lem  37974  hgmapvvlem3  38068  suprleubrd  38512  suprlubrd  38516  imo72b2  38522
  Copyright terms: Public domain W3C validator