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

Theorem mpdan 650
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 20 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan2  653  mpjaodan  762  mpd3an3  1280  eueq2  3076  csbiegf  3259  difsnb  3908  reusv3i  4697  onsucuni  4775  fvmpt3  5775  ffvelrnd  5838  fnressn  5885  f1oiso2  6039  riota5f  6541  riotasvdOLD  6560  seqomlem2  6675  oaordi  6756  nnaordi  6828  qsdisj  6948  dom2lem  7114  canth2g  7228  limenpsi  7249  php4  7261  onfin  7264  sucxpdom  7285  xpfi  7345  dmfi  7356  pwfilem  7367  pwfi  7368  fiin  7393  supiso  7441  ordiso2  7448  wemaplem2  7480  wdom2d  7512  infeq5  7556  cantnfp1lem3  7600  cantnflem1d  7608  r1val1  7676  rankwflemb  7683  onenon  7800  cardonle  7808  sdomsdomcardi  7822  acni  7890  cardaleph  7934  cdaen  8017  cdainf  8036  infcda1  8037  pwsdompw  8048  infdif  8053  cfval  8091  fin34  8234  fin1a2lem1  8244  fin1a2  8259  ttukeylem6  8358  sdomsdomcard  8399  canth3  8400  fpwwe2  8482  canthwelem  8489  gchcda1  8495  pwfseqlem4  8501  gchcdaidm  8507  gchxpidm  8508  tskwe2  8612  rankcf  8616  tskuni  8622  gruxp  8646  dmrecnq  8809  lterpq  8811  archnq  8821  reclem3pr  8890  reclem4pr  8891  0idsr  8936  lep1  9813  ledivp1  9876  supmul1  9937  suprzcl  10313  uz11  10472  zmin  10534  zbtwnre  10536  rpnnen1lem4  10567  rpnnen1lem5  10568  xnegid  10786  xleadd1a  10796  xlt2add  10803  xmullem  10807  xmulgt0  10826  xmulasslem3  10829  xlemul1a  10831  xadddilem  10837  xadddi  10838  xadddi2  10840  xrsupss  10851  xrinfmss  10852  supxrre  10870  infmxrre  10878  eluzfz2  11029  fzsuc  11060  fzsuc2  11068  fzp1disj  11069  fzneuz  11091  fllep1  11173  fraclt1  11174  fracle1  11175  fracge0  11176  flhalf  11194  ceige  11196  ceim1l  11197  fldiv  11204  modval  11215  seqeq1  11289  expubnd  11403  iexpcyc  11448  faclbnd4lem3  11549  faclbnd4lem4  11550  shftfval  11848  shftcan1  11861  reval  11874  cjmulrcl  11912  addcj  11916  absval  12006  absneg  12045  abscj  12047  sqabsadd  12050  sqabssub  12051  leabs  12067  sqreulem  12126  lo1res  12316  o1of2  12369  o1rlimmul  12375  sumrb  12470  flo1  12597  trirecip  12605  efcan  12660  efi4p  12701  resin4p  12702  recos4p  12703  sincossq  12740  ruclem10  12801  iddvds  12826  1dvds  12827  2ebits  12922  1idssfct  13048  exprmfct  13073  eulerthlem2  13134  odzphi  13145  pcprendvds  13177  pcmpt  13224  vdwlem8  13319  0ram2  13352  pwsvscaval  13680  issect2  13943  homarel  14154  latjcom  14451  latlej1  14452  latlej2  14453  latmcom  14467  latmle1  14468  latmle2  14469  grprcan  14801  isgrpid2  14804  grpinvid  14819  mulgnn0z  14873  0subg  14928  divs0  14961  ghmker  14994  symginv  15068  odval2  15152  odmulg2  15154  slwpgp  15210  pj1eq  15295  efgtf  15317  frgpinv  15359  frgpup2  15371  mulgnn0di  15411  cnaddablx  15444  cnaddabl  15445  zaddablx  15446  dprdfadd  15541  dpjidcl  15579  dpjlid  15582  pgpfac1lem3  15598  rnglz  15663  rngrz  15664  1unit  15726  unitgrpid  15737  1rinv  15747  irredn0  15771  irredneg  15778  isdrng2  15808  abv0  15882  abv1z  15883  abvneg  15885  lsssn0  15987  lspsn0  16047  lsp0  16048  lmhmvsca  16084  lmhmrnlss  16089  lmhmkerlss  16090  lsppratlem5  16186  rsp1  16258  rlmassa  16348  asclpropd  16367  psrvscaval  16419  psrdi  16433  psrdir  16434  mplsubglem  16461  mplvscaval  16474  coe1sclmulfv  16638  cnfldneg  16690  zcyg  16735  chrid  16771  chrrhm  16775  ip0r  16831  ocvlss  16862  ocv1  16869  cctop  17033  cldval  17050  ntrfval  17051  clsfval  17052  cmclsopn  17089  opncldf3  17113  neifval  17126  lpfval  17165  cnrmnrm  17387  tx1cn  17602  tx2cn  17603  idqtop  17699  kqtopon  17720  kqid  17721  kqcld  17728  hmphen2  17792  filssufil  17905  ufileu  17912  alexsublem  18036  symgtgp  18092  ustuqtop4  18235  ustuqtop5  18236  cstucnd  18275  isxmet2d  18318  metustexhalfOLD  18554  metustexhalf  18555  nm0  18634  rlmnlm  18685  nmolb  18712  metdseq0  18845  iocopnst  18926  icccvx  18936  pi1xfrval  19040  clmvneg1  19077  ipcau2  19152  tchcphlem1  19153  tchcphlem2  19154  cmetcaulem  19202  ivthicc  19316  ovolicc2lem3  19376  ovolicc2lem4  19377  mbfmulc2lem  19500  i1fpos  19559  mbfi1fseqlem3  19570  mbfi1fseqlem4  19571  itg2ge0  19588  dvres2  19760  dvaddbr  19785  dvmulbr  19786  dvcobr  19793  c1lip1  19842  dvivth  19855  dvfsumlem4  19874  ftc1a  19882  ftc1lem6  19886  evl1var  19913  uc1pmon1p  20035  ig1pval2  20057  dgradd2  20147  dgrcolem2  20153  plydivlem4  20174  plydiveu  20176  elqaalem3  20199  qaa  20201  ulmdvlem1  20277  abelthlem6  20313  abelthlem7  20315  reeff1o  20324  coseq00topi  20371  tanabsge  20375  eflogeq  20457  logcnlem3  20496  atantan  20724  atanbnd  20727  cvxcl  20784  jensenlem2  20787  harmonicbnd4  20810  sgmnncl  20891  dchrptlem2  21010  1lgs  21082  lgs1  21083  dchrisumlem2  21145  dchrisum0lem2a  21172  selberg2lem  21205  pntrsumo1  21220  pntrsumbnd  21221  pntpbnd1  21241  pntlemr  21257  pntlemj  21258  ostthlem1  21282  padicabvf  21286  cusgraexilem2  21437  cusgraexi  21438  cusgrasizeinds  21446  eupacl  21652  eupapf  21655  eupaseg  21656  isgrpoi  21747  grpoinvfval  21773  grpoinvid  21781  grpodivfval  21791  gxfval  21806  gxid  21822  issubgo  21852  cnaddablo  21899  ghomid  21914  rngolz  21950  rngorz  21951  rngosn6  21977  vcz  22010  vcoprne  22019  nvz0  22118  sspz  22195  lno0  22218  nmobndi  22237  ipasslem2  22294  shunssi  22831  ococin  22871  ssjo  22910  pjocini  23161  nlfnval  23345  lncnopbd  23501  riesz3i  23526  cnlnadjlem7  23537  pjclem4  23663  pj3si  23671  hstoc  23686  hstnmoc  23687  hstoh  23696  hst0  23697  mdsl2i  23786  chirredlem3  23856  chirredlem4  23857  dmdbr5ati  23886  rexunirn  23939  abfmpel  24028  xrpxdivcld  24142  ofld0le1  24203  esumcst  24416  esumcvg  24437  sigaval  24454  measval  24513  probfinmeasb  24648  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemsi  24733  ballotlemfrci  24746  erdszelem7  24844  erdszelem8  24845  cvmliftlem10  24942  cvmliftlem13  24944  cvmlift2lem9  24959  cvmlift3lem6  24972  cvmlift3lem7  24973  cvmlift3lem9  24975  ghomgrpilem2  25058  prodrblem2  25218  dfrdg2  25374  dftrpred3g  25458  wfrlem5  25482  frrlem5  25507  bdayval  25524  ontopbas  26090  supaddc  26145  ismblfin  26154  cnambfre  26162  bddiblnc  26182  ftc1cnnc  26186  cldregopn  26232  islocfin  26274  tailfval  26299  filnetlem3  26307  filnetlem4  26308  ismtyres  26415  heiborlem8  26425  rngonegmn1l  26463  rngonegmn1r  26464  rngoneglmul  26465  rngonegrmul  26466  idlnegcl  26530  0idl  26533  0rngo  26535  keridl  26540  smprngopr  26560  fvtresfn  26642  mzpval  26687  mzpindd  26701  pellex  26796  2nn0ind  26906  jm2.26lem3  26970  pw2f1o2val  27008  wepwsolem  27014  fnwe2lem3  27025  lnmfg  27056  dgrsub2  27215  mpaaeu  27231  flcidc  27255  pmtrfrn  27276  mamuvs1  27339  mamuvs2  27340  dvconstbi  27427  itgsin0pilem1  27619  stoweidlem22  27646  stoweidlem32  27656  stoweidlem35  27659  stoweidlem36  27660  stoweidlem37  27661  stoweidlem43  27667  stoweidlem50  27674  wallispilem5  27693  stirlinglem2  27699  stirlinglem3  27700  stirlinglem4  27701  stirlinglem8  27705  stirlinglem11  27708  stirlinglem12  27709  stirlinglem14  27711  stirlinglem15  27712  frgrancvvdeqlemC  28150  frghash2spot  28174  bnj1006  29048  bnj1110  29069  bnj1253  29104  bnj1280  29107  bnj1463  29142  bnj1312  29145  lubunNEW  29468  lshpne0  29481  lkrval  29583  ldualvaddval  29626  ldualvsval  29633  lub0N  29684  glb0N  29688  opoc1  29697  pmap0  30259  pmap1N  30261  pexmidALTN  30472  trlval2  30657  cdleme31fv  30884  cdlemefrs32fva  30894  cdlemg27b  31190  cdlemk40  31411  erngdvlem4  31485  erng0g  31488  erngdvlem4-rN  31493  dvalveclem  31520  dvh0g  31606  dih0cnv  31778  dih1rn  31782  dih1cnv  31783  doch0  31853  doch1  31854  lcfl7lem  31994  mapdheq  32223  hdmap1eq  32297  hdmapval2lem  32329  hgmapvvlem3  32423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator