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

Theorem mpdan 661
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 654 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  664  mpjaodan  777  mpd3an3  1308  eueq2  3122  csbiegf  3300  difsnb  4003  reusv3i  4487  fvtresfn  5763  fvmpt3  5765  ffvelrnd  5832  fnressn  5881  f1oiso2  6030  riota5f  6065  onsucuni  6428  seqomlem2  6892  oaordi  6973  nnaordi  7045  qsdisj  7165  dom2lem  7337  canth2g  7453  limenpsi  7474  php4  7486  onfin  7489  sucxpdom  7510  xpfi  7571  dmfi  7582  pwfilem  7593  pwfi  7594  fiin  7660  supiso  7710  ordiso2  7717  wemaplem2  7749  wdom2d  7783  infeq5  7831  cantnfp1lem3  7876  cantnflem1d  7884  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  r1val1  7981  rankwflemb  7988  onenon  8107  cardonle  8115  sdomsdomcardi  8129  acni  8203  cardaleph  8247  cdaen  8330  cdainf  8349  infcda1  8350  pwsdompw  8361  infdif  8366  cfval  8404  fin34  8547  fin1a2lem1  8557  fin1a2  8572  ttukeylem6  8671  sdomsdomcard  8712  canth3  8713  fpwwe2  8798  canthwelem  8805  gchcda1  8811  pwfseqlem4  8817  gchcdaidm  8823  gchxpidm  8824  tskwe2  8928  rankcf  8932  tskuni  8938  gruxp  8962  dmrecnq  9125  lterpq  9127  archnq  9137  reclem3pr  9206  reclem4pr  9207  0idsr  9252  lep1  10156  ledivp1  10222  supmul1  10283  suprzcl  10709  uz11  10871  zmin  10937  zbtwnre  10939  rpnnen1lem4  10970  rpnnen1lem5  10971  xnegid  11194  xleadd1a  11204  xlt2add  11211  xmullem  11215  xmulgt0  11234  xmulasslem3  11237  xlemul1a  11239  xadddilem  11245  xadddi  11246  xadddi2  11248  xrsupss  11259  xrinfmss  11260  supxrre  11278  infmxrre  11286  eluzfz2  11446  fzsuc  11489  fzsuc2  11499  fzp1disj  11500  fzneuz  11525  fllep1  11635  fraclt1  11636  fracle1  11637  fracge0  11638  flhalf  11658  ceige  11668  ceim1l  11670  fldiv  11683  modval  11694  seqeq1  11793  expubnd  11908  iexpcyc  11954  faclbnd4lem3  12055  faclbnd4lem4  12056  swrdccat3blem  12370  cshwn  12418  shftfval  12543  shftcan1  12556  reval  12579  cjmulrcl  12617  addcj  12621  absval  12711  absneg  12750  abscj  12752  sqabsadd  12755  sqabssub  12756  leabs  12772  sqreulem  12831  lo1res  13021  o1of2  13074  o1rlimmul  13080  sumrb  13174  flo1  13300  trirecip  13308  efcan  13363  efi4p  13404  resin4p  13405  recos4p  13406  sincossq  13443  ruclem10  13504  iddvds  13529  1dvds  13530  2ebits  13626  1idssfct  13752  exprmfct  13779  eulerthlem2  13840  odzphi  13851  pcprendvds  13890  pcmpt  13937  vdwlem8  14032  0ram2  14065  pwsvscaval  14416  issect2  14676  homarel  14887  joinfval  15154  meetfval  15168  latjcom  15212  latmcom  15228  grprcan  15551  isgrpid2  15554  grpinvid  15569  mulgnn0z  15627  0subg  15686  divs0  15719  ghmker  15752  symginv  15887  symgfixfvh  15921  pmtrfrn  15944  odmulg2  16036  slwpgp  16092  pj1eq  16177  efgtf  16199  frgpinv  16241  frgpup2  16253  mulgnn0di  16293  cnaddablx  16328  cnaddabl  16329  zaddablx  16330  dprdfadd  16484  dprdfaddOLD  16491  dpjidcl  16531  dpjlid  16534  dpjidclOLD  16538  pgpfac1lem3  16552  rnglz  16617  rngrz  16618  1unit  16684  unitgrpid  16695  1rinv  16705  irredn0  16729  irredneg  16736  isdrng2  16766  abv0  16840  abv1z  16841  abvneg  16843  lsssn0  16951  lspsn0  17011  lsp0  17012  lmhmvsca  17048  lmhmrnlss  17053  lmhmkerlss  17054  lsppratlem5  17154  rsp1  17228  rlmassa  17319  asclpropd  17338  snifpsrbag  17367  psrvscaval  17397  psrdi  17413  psrdir  17414  mplsubglem  17444  mplsubglemOLD  17446  mplvscaval  17461  coe1sclmulfv  17634  cnfldneg  17686  zringcyg  17749  zcyg  17754  chrid  17800  chrrhm  17804  ip0r  17908  ocvlss  17939  ocv1  17946  mamuvs1  18151  mamuvs2  18152  matecl  18168  submaval0  18233  mdetrsca  18252  maduval  18286  minmar1val0  18295  cctop  18452  cldval  18469  ntrfval  18470  clsfval  18471  cmclsopn  18508  opncldf3  18532  neifval  18545  lpfval  18584  cnrmnrm  18807  tx1cn  19024  tx2cn  19025  idqtop  19121  kqtopon  19142  kqid  19143  kqcld  19150  hmphen2  19214  filssufil  19327  ufileu  19334  alexsublem  19458  symgtgp  19514  ustuqtop4  19661  ustuqtop5  19662  cstucnd  19701  isxmet2d  19744  metustexhalfOLD  19980  metustexhalf  19981  nm0  20060  rlmnlm  20111  nmolb  20138  metdseq0  20272  iocopnst  20354  icccvx  20364  pi1xfrval  20468  clmvneg1  20505  ipcau2  20591  tchcphlem1  20592  tchcphlem2  20593  cmetcaulem  20641  ivthicc  20784  ovolicc2lem3  20844  ovolicc2lem4  20845  mbfmulc2lem  20967  i1fpos  21026  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  itg2ge0  21055  dvres2  21229  dvaddbr  21254  dvmulbr  21255  dvcobr  21262  c1lip1  21311  dvivth  21324  dvfsumlem4  21343  ftc1a  21351  ftc1lem6  21355  evl1var  21383  uc1pmon1p  21508  ig1pval2  21530  dgradd2  21620  dgrcolem2  21626  plydivlem4  21647  plydiveu  21649  elqaalem3  21672  qaa  21674  ulmdvlem1  21750  abelthlem6  21786  abelthlem7  21788  reeff1o  21797  coseq00topi  21849  tanabsge  21853  eflogeq  21935  logcnlem3  21974  atantan  22203  atanbnd  22206  cvxcl  22263  jensenlem2  22266  harmonicbnd4  22289  sgmnncl  22370  dchrptlem2  22489  1lgs  22561  lgs1  22562  dchrisumlem2  22624  dchrisum0lem2a  22651  selberg2lem  22684  pntrsumo1  22699  pntrsumbnd  22700  pntpbnd1  22720  pntlemr  22736  pntlemj  22737  ostthlem1  22761  padicabvf  22765  tglineeltr  22908  ttgval  22944  xmstrkgc  22955  cusgraexilem2  23198  cusgraexi  23199  cusgrasizeinds  23207  eupacl  23413  eupapf  23416  eupaseg  23417  isgrpoi  23508  grpoinvfval  23534  grpoinvid  23542  grpodivfval  23552  gxfval  23567  gxid  23583  issubgo  23613  cnaddablo  23660  ghomid  23675  rngolz  23711  rngorz  23712  rngosn6  23738  vcz  23771  vcoprne  23780  nvz0  23879  sspz  23956  lno0  23979  nmobndi  23998  ipasslem2  24055  shunssi  24594  ococin  24634  ssjo  24673  pjocini  24924  nlfnval  25108  lncnopbd  25264  riesz3i  25289  cnlnadjlem7  25300  pjclem4  25426  pj3si  25434  hstoc  25449  hstnmoc  25450  hstoh  25459  hst0  25460  mdsl2i  25549  chirredlem3  25619  chirredlem4  25620  dmdbr5ati  25649  rexunirn  25699  fcnvgreu  25815  xrpxdivcld  25933  omndmul2  25999  omndmul  26001  isarchi3  26028  orng0le1  26133  esumcst  26368  esumcvg  26389  sigaval  26407  measval  26466  eulerpartlemgvv  26607  probfinmeasb  26660  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemsi  26745  ballotlemfrci  26758  signspval  26801  signlem0  26836  erdszelem7  26933  erdszelem8  26934  cvmliftlem10  27031  cvmliftlem13  27033  cvmlift2lem9  27048  cvmlift3lem6  27061  cvmlift3lem7  27062  cvmlift3lem9  27064  ghomgrpilem2  27152  prodrblem2  27291  dfrdg2  27456  dftrpred3g  27544  wfrlem5  27575  frrlem5  27619  bdayval  27636  ontopbas  28122  supaddc  28261  ismblfin  28276  cnambfre  28284  bddiblnc  28306  ftc1cnnc  28310  dvasin  28324  cldregopn  28370  islocfin  28412  tailfval  28437  filnetlem3  28445  filnetlem4  28446  ismtyres  28551  heiborlem8  28561  rngonegmn1l  28599  rngonegmn1r  28600  rngoneglmul  28601  rngonegrmul  28602  idlnegcl  28666  0idl  28669  0rngo  28671  keridl  28676  smprngopr  28696  mzpval  28913  mzpindd  28927  pellex  29021  2nn0ind  29131  jm2.26lem3  29195  pw2f1o2val  29233  wepwsolem  29239  fnwe2lem3  29250  lnmfg  29280  dgrsub2  29336  mpaaeu  29352  flcidc  29376  dvconstbi  29453  itgsin0pilem1  29636  stoweidlem22  29663  stoweidlem32  29673  stoweidlem35  29676  stoweidlem36  29677  stoweidlem37  29678  stoweidlem43  29684  stoweidlem50  29691  wallispilem5  29710  stirlinglem2  29716  stirlinglem3  29717  stirlinglem4  29718  stirlinglem8  29722  stirlinglem11  29725  stirlinglem12  29726  stirlinglem14  29728  stirlinglem15  29729  wwlksubclwwlk  30312  erclwwlkref  30329  erclwwlknref  30345  usgrauvtxvd  30376  vdcusgra  30377  frgrancvvdeqlemC  30478  frghash2spot  30502  nzrneg1ne0  30611  coe1id  30630  matvscacell  30642  bnj1006  31654  bnj1110  31675  bnj1253  31710  bnj1280  31713  bnj1463  31748  bnj1312  31751  lshpne0  32204  lkrval  32306  ldualvaddval  32349  ldualvsval  32356  opoc1  32420  pmap0  32982  pmap1N  32984  pexmidALTN  33195  cdleme31fv  33607  cdlemg27b  33913  erngdvlem4  34208  erng0g  34211  erngdvlem4-rN  34216  dvalveclem  34243  dvh0g  34329  dih0cnv  34501  dih1rn  34505  dih1cnv  34506  doch0  34576  doch1  34577  lcfl7lem  34717  mapdheq  34946  hdmap1eq  35020  hdmapval2lem  35052  hgmapvvlem3  35146
  Copyright terms: Public domain W3C validator