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

Theorem mpdan 651
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 21 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpan2  654  mpjaodan  763  mpd3an3  1281  eueq2  3114  csbiegf  3290  difsnb  3964  reusv3i  4759  onsucuni  4837  fvmpt3  5837  ffvelrnd  5900  fnressn  5947  f1oiso2  6101  riota5f  6603  riotasvdOLD  6622  seqomlem2  6737  oaordi  6818  nnaordi  6890  qsdisj  7010  dom2lem  7176  canth2g  7290  limenpsi  7311  php4  7323  onfin  7326  sucxpdom  7347  xpfi  7407  dmfi  7418  pwfilem  7430  pwfi  7431  fiin  7456  supiso  7506  ordiso2  7513  wemaplem2  7545  wdom2d  7577  infeq5  7621  cantnfp1lem3  7665  cantnflem1d  7673  r1val1  7741  rankwflemb  7748  onenon  7867  cardonle  7875  sdomsdomcardi  7889  acni  7957  cardaleph  8001  cdaen  8084  cdainf  8103  infcda1  8104  pwsdompw  8115  infdif  8120  cfval  8158  fin34  8301  fin1a2lem1  8311  fin1a2  8326  ttukeylem6  8425  sdomsdomcard  8466  canth3  8467  fpwwe2  8549  canthwelem  8556  gchcda1  8562  pwfseqlem4  8568  gchcdaidm  8574  gchxpidm  8575  tskwe2  8679  rankcf  8683  tskuni  8689  gruxp  8713  dmrecnq  8876  lterpq  8878  archnq  8888  reclem3pr  8957  reclem4pr  8958  0idsr  9003  lep1  9880  ledivp1  9943  supmul1  10004  suprzcl  10380  uz11  10539  zmin  10601  zbtwnre  10603  rpnnen1lem4  10634  rpnnen1lem5  10635  xnegid  10853  xleadd1a  10863  xlt2add  10870  xmullem  10874  xmulgt0  10893  xmulasslem3  10896  xlemul1a  10898  xadddilem  10904  xadddi  10905  xadddi2  10907  xrsupss  10918  xrinfmss  10919  supxrre  10937  infmxrre  10945  eluzfz2  11096  fzsuc  11127  fzsuc2  11135  fzp1disj  11136  fzneuz  11159  fllep1  11241  fraclt1  11242  fracle1  11243  fracge0  11244  flhalf  11262  ceige  11264  ceim1l  11265  fldiv  11272  modval  11283  seqeq1  11357  expubnd  11471  iexpcyc  11516  faclbnd4lem3  11617  faclbnd4lem4  11618  shftfval  11916  shftcan1  11929  reval  11942  cjmulrcl  11980  addcj  11984  absval  12074  absneg  12113  abscj  12115  sqabsadd  12118  sqabssub  12119  leabs  12135  sqreulem  12194  lo1res  12384  o1of2  12437  o1rlimmul  12443  sumrb  12538  flo1  12665  trirecip  12673  efcan  12728  efi4p  12769  resin4p  12770  recos4p  12771  sincossq  12808  ruclem10  12869  iddvds  12894  1dvds  12895  2ebits  12990  1idssfct  13116  exprmfct  13141  eulerthlem2  13202  odzphi  13213  pcprendvds  13245  pcmpt  13292  vdwlem8  13387  0ram2  13420  pwsvscaval  13748  issect2  14011  homarel  14222  latjcom  14519  latlej1  14520  latlej2  14521  latmcom  14535  latmle1  14536  latmle2  14537  grprcan  14869  isgrpid2  14872  grpinvid  14887  mulgnn0z  14941  0subg  14996  divs0  15029  ghmker  15062  symginv  15136  odval2  15220  odmulg2  15222  slwpgp  15278  pj1eq  15363  efgtf  15385  frgpinv  15427  frgpup2  15439  mulgnn0di  15479  cnaddablx  15512  cnaddabl  15513  zaddablx  15514  dprdfadd  15609  dpjidcl  15647  dpjlid  15650  pgpfac1lem3  15666  rnglz  15731  rngrz  15732  1unit  15794  unitgrpid  15805  1rinv  15815  irredn0  15839  irredneg  15846  isdrng2  15876  abv0  15950  abv1z  15951  abvneg  15953  lsssn0  16055  lspsn0  16115  lsp0  16116  lmhmvsca  16152  lmhmrnlss  16157  lmhmkerlss  16158  lsppratlem5  16254  rsp1  16326  rlmassa  16416  asclpropd  16435  psrvscaval  16487  psrdi  16501  psrdir  16502  mplsubglem  16529  mplvscaval  16542  coe1sclmulfv  16706  cnfldneg  16758  zcyg  16803  chrid  16839  chrrhm  16843  ip0r  16899  ocvlss  16930  ocv1  16937  cctop  17101  cldval  17118  ntrfval  17119  clsfval  17120  cmclsopn  17157  opncldf3  17181  neifval  17194  lpfval  17233  cnrmnrm  17456  tx1cn  17672  tx2cn  17673  idqtop  17769  kqtopon  17790  kqid  17791  kqcld  17798  hmphen2  17862  filssufil  17975  ufileu  17982  alexsublem  18106  symgtgp  18162  ustuqtop4  18305  ustuqtop5  18306  cstucnd  18345  isxmet2d  18388  metustexhalfOLD  18624  metustexhalf  18625  nm0  18704  rlmnlm  18755  nmolb  18782  metdseq0  18915  iocopnst  18996  icccvx  19006  pi1xfrval  19110  clmvneg1  19147  ipcau2  19222  tchcphlem1  19223  tchcphlem2  19224  cmetcaulem  19272  ivthicc  19386  ovolicc2lem3  19446  ovolicc2lem4  19447  mbfmulc2lem  19568  i1fpos  19627  mbfi1fseqlem3  19638  mbfi1fseqlem4  19639  itg2ge0  19656  dvres2  19830  dvaddbr  19855  dvmulbr  19856  dvcobr  19863  c1lip1  19912  dvivth  19925  dvfsumlem4  19944  ftc1a  19952  ftc1lem6  19956  evl1var  19983  uc1pmon1p  20105  ig1pval2  20127  dgradd2  20217  dgrcolem2  20223  plydivlem4  20244  plydiveu  20246  elqaalem3  20269  qaa  20271  ulmdvlem1  20347  abelthlem6  20383  abelthlem7  20385  reeff1o  20394  coseq00topi  20441  tanabsge  20445  eflogeq  20527  logcnlem3  20566  atantan  20794  atanbnd  20797  cvxcl  20854  jensenlem2  20857  harmonicbnd4  20880  sgmnncl  20961  dchrptlem2  21080  1lgs  21152  lgs1  21153  dchrisumlem2  21215  dchrisum0lem2a  21242  selberg2lem  21275  pntrsumo1  21290  pntrsumbnd  21291  pntpbnd1  21311  pntlemr  21327  pntlemj  21328  ostthlem1  21352  padicabvf  21356  cusgraexilem2  21507  cusgraexi  21508  cusgrasizeinds  21516  eupacl  21722  eupapf  21725  eupaseg  21726  isgrpoi  21817  grpoinvfval  21843  grpoinvid  21851  grpodivfval  21861  gxfval  21876  gxid  21892  issubgo  21922  cnaddablo  21969  ghomid  21984  rngolz  22020  rngorz  22021  rngosn6  22047  vcz  22080  vcoprne  22089  nvz0  22188  sspz  22265  lno0  22288  nmobndi  22307  ipasslem2  22364  shunssi  22901  ococin  22941  ssjo  22980  pjocini  23231  nlfnval  23415  lncnopbd  23571  riesz3i  23596  cnlnadjlem7  23607  pjclem4  23733  pj3si  23741  hstoc  23756  hstnmoc  23757  hstoh  23766  hst0  23767  mdsl2i  23856  chirredlem3  23926  chirredlem4  23927  dmdbr5ati  23956  rexunirn  24009  abfmpel  24098  xrpxdivcld  24212  ofld0le1  24273  esumcst  24486  esumcvg  24507  sigaval  24524  measval  24583  probfinmeasb  24718  ballotlemfc0  24781  ballotlemfcc  24782  ballotlemsi  24803  ballotlemfrci  24816  erdszelem7  24914  erdszelem8  24915  cvmliftlem10  25012  cvmliftlem13  25014  cvmlift2lem9  25029  cvmlift3lem6  25042  cvmlift3lem7  25043  cvmlift3lem9  25045  ghomgrpilem2  25128  prodrblem2  25288  dfrdg2  25454  dftrpred3g  25542  wfrlem5  25573  frrlem5  25617  bdayval  25634  ontopbas  26209  supaddc  26269  ismblfin  26283  cnambfre  26291  bddiblnc  26313  ftc1cnnc  26317  cldregopn  26372  islocfin  26414  tailfval  26439  filnetlem3  26447  filnetlem4  26448  ismtyres  26555  heiborlem8  26565  rngonegmn1l  26603  rngonegmn1r  26604  rngoneglmul  26605  rngonegrmul  26606  idlnegcl  26670  0idl  26673  0rngo  26675  keridl  26680  smprngopr  26700  fvtresfn  26782  mzpval  26827  mzpindd  26841  pellex  26936  2nn0ind  27046  jm2.26lem3  27110  pw2f1o2val  27148  wepwsolem  27154  fnwe2lem3  27165  lnmfg  27195  dgrsub2  27354  mpaaeu  27370  flcidc  27394  pmtrfrn  27415  mamuvs1  27478  mamuvs2  27479  dvconstbi  27566  itgsin0pilem1  27758  stoweidlem22  27785  stoweidlem32  27795  stoweidlem35  27798  stoweidlem36  27799  stoweidlem37  27800  stoweidlem43  27806  stoweidlem50  27813  wallispilem5  27832  stirlinglem2  27838  stirlinglem3  27839  stirlinglem4  27840  stirlinglem8  27844  stirlinglem11  27847  stirlinglem12  27848  stirlinglem14  27850  stirlinglem15  27851  swrdccat3blem  28276  cshwn  28297  usgrauvtxvd  28452  vdcusgra  28453  frgrancvvdeqlemC  28526  frghash2spot  28550  bnj1006  29428  bnj1110  29449  bnj1253  29484  bnj1280  29487  bnj1463  29522  bnj1312  29525  lubunNEW  29869  lshpne0  29882  lkrval  29984  ldualvaddval  30027  ldualvsval  30034  lub0N  30085  glb0N  30089  opoc1  30098  pmap0  30660  pmap1N  30662  pexmidALTN  30873  trlval2  31058  cdleme31fv  31285  cdlemefrs32fva  31295  cdlemg27b  31591  cdlemk40  31812  erngdvlem4  31886  erng0g  31889  erngdvlem4-rN  31894  dvalveclem  31921  dvh0g  32007  dih0cnv  32179  dih1rn  32183  dih1cnv  32184  doch0  32254  doch1  32255  lcfl7lem  32395  mapdheq  32624  hdmap1eq  32698  hdmapval2lem  32730  hgmapvvlem3  32824
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 179  df-an 362
  Copyright terms: Public domain W3C validator