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

Theorem mpdan 698
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 (𝜑𝜓)
mpdan.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpdan (𝜑𝜒)

Proof of Theorem mpdan
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 mpdan.1 . 2 (𝜑𝜓)
3 mpdan.2 . 2 ((𝜑𝜓) → 𝜒)
41, 2, 3syl2anc 690 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  mpidan  700  mpan2  702  mpjaodan  822  mpd3an3  1416  eueq2  3346  csbiegf  3522  difsnb  4277  reusv3i  4796  fvtresfn  6178  fvmpt3  6180  ffvelrnd  6253  fnressn  6308  fsnex  6416  f1oiso2  6480  riota5f  6513  onsucuni  6898  wfrlem5  7284  seqomlem2  7411  oaordi  7491  nnaordi  7563  qsdisj  7689  dom2lem  7859  canth2g  7977  limenpsi  7998  php4  8010  onfin  8014  sucxpdom  8032  xpfi  8094  dmfi  8107  pwfilem  8121  pwfi  8122  fiin  8189  supiso  8242  ordiso2  8281  wdom2d  8346  infeq5  8395  cantnfp1lem3  8438  cantnflem1d  8446  rankwflemb  8517  onenon  8636  cardonle  8644  sdomsdomcardi  8658  acni  8729  cardaleph  8773  cdaen  8856  cdainf  8875  infcda1  8876  pwsdompw  8887  infdif  8892  cfval  8930  fin34  9073  fin1a2lem1  9083  fin1a2  9098  ttukeylem6  9197  sdomsdomcard  9239  canth3  9240  fpwwe2  9322  canthwelem  9329  gchcda1  9335  pwfseqlem4  9341  gchcdaidm  9347  gchxpidm  9348  tskwe2  9452  rankcf  9456  tskuni  9462  gruxp  9486  dmrecnq  9647  lterpq  9649  archnq  9659  reclem3pr  9728  reclem4pr  9729  0idsr  9775  lep1  10714  ledivp1  10777  negfi  10823  supaddc  10840  supmul1  10842  suprzcl  11292  uz11  11545  zmin  11619  zbtwnre  11621  rpnnen1lem4  11652  rpnnen1lem5  11653  rpnnen1lem4OLD  11658  rpnnen1lem5OLD  11659  xnegid  11904  xrsupss  11970  xrinfmss  11971  supxrre  11988  infxrre  11997  eluzfz2  12178  fzsuc  12216  fzsuc2  12226  fzp1disj  12227  fzneuz  12248  nn0p1elfzo  12336  fllep1  12422  fraclt1  12423  fracle1  12424  fracge0  12425  flhalf  12451  ceige  12464  ceim1l  12466  fldiv  12479  modval  12490  suppssfz  12614  seqeq1  12624  expubnd  12741  iexpcyc  12789  binom2sub1  12802  faclbnd4lem3  12902  swrdid  13229  swrdccat3blem  13295  cshwn  13343  cshimadifsn  13375  cshimadifsn0  13376  trclexlem  13530  shftfval  13607  shftcan1  13620  reval  13643  cjmulrcl  13681  addcj  13685  absval  13775  absneg  13814  abscj  13816  sqabsadd  13819  sqabssub  13820  leabs  13836  sqreulem  13896  lo1res  14087  o1of2  14140  o1rlimmul  14146  flo1  14374  trirecip  14383  efcan  14614  efi4p  14655  resin4p  14656  recos4p  14657  sincossq  14694  ruclem10  14756  iddvds  14782  1dvds  14783  2ebits  14956  lcmftp  15136  coprmgcdb  15149  1idssfct  15180  exprmfct  15203  eulerthlem2  15274  odzphi  15288  pcprendvds  15332  pcmpt  15383  vdwlem8  15479  0ram2  15512  prmgaplem7  15548  pwsvscaval  15927  issect2  16186  2initoinv  16432  initoeu1  16433  initoeu2lem1  16436  initoeu2  16438  2termoinv  16439  termoeu1  16440  homarel  16458  joinfval  16773  meetfval  16787  latjcom  16831  latmcom  16847  sgrp2nmndlem5  17188  grprcan  17227  isgrpid2  17230  grpinvid  17248  mulgnn0z  17339  0subg  17391  qus0  17424  ghmker  17458  symginv  17594  pmtrfrn  17650  odmulg2  17744  slwpgp  17800  pj1eq  17885  efgtf  17907  frgpinv  17949  frgpup2  17961  mulgnn0di  18003  cnaddablx  18043  cnaddabl  18044  zaddablx  18047  dprdfadd  18191  dpjidcl  18229  dpjlid  18232  pgpfac1lem3  18248  srgen1zr  18302  ringlz  18359  ringrz  18360  1unit  18430  unitgrpid  18441  1rinv  18451  irredn0  18475  irredneg  18482  isdrng2  18529  abv0  18603  abv1z  18604  abvneg  18606  lmodfopne  18673  lsssn0  18718  lspsn0  18778  lsp0  18779  lmhmvsca  18815  lmhmrnlss  18820  lmhmkerlss  18821  lsppratlem5  18921  rsp1  18994  ringen1zr  19047  rlmassa  19096  snifpsrbag  19136  psrvscaval  19162  psrdi  19176  psrdir  19177  mplsubglem  19204  mplvscaval  19218  coe1sclmulfv  19423  ply1idvr1  19433  evl1var  19470  cnfldneg  19540  zringcyg  19604  chrid  19642  chrrhm  19646  ip0r  19749  ocvlss  19783  ocv1  19790  mamuvs1  19978  mamuvs2  19979  matecl  19998  matvscacell  20009  mat0scmat  20111  submaval0  20153  mdetrsca  20176  maduval  20211  minmar1val0  20220  pmatcollpw3fi1lem2  20359  chfacfscmulgsum  20432  chfacfpmmulgsum  20436  chcoeffeqlem  20457  cayleyhamilton0  20461  cayleyhamiltonALT  20463  cctop  20568  cldval  20585  ntrfval  20586  clsfval  20587  cmclsopn  20624  opncldf3  20648  neifval  20661  lpfval  20700  cnrmnrm  20923  islocfin  21078  tx1cn  21170  idqtop  21267  kqtopon  21288  kqid  21289  kqcld  21296  hmphen2  21360  filssufil  21474  ufileu  21481  alexsublem  21606  symgtgp  21663  ustuqtop4  21806  cstucnd  21846  metustexhalf  22119  nm0  22191  rlmnlm  22250  nmolb  22279  metdseq0  22413  pi1xfrval  22610  clmvneg1  22655  clmvsubval  22665  ipcau2  22786  tchcphlem1  22787  tchcphlem2  22788  cmetcaulem  22839  ovolicc2lem3  23039  ovolicc2lem4  23040  mbfmulc2lem  23165  i1fpos  23224  mbfi1fseqlem3  23235  mbfi1fseqlem4  23236  itg2ge0  23253  dvres2  23427  dvaddbr  23452  dvmulbr  23453  dvcobr  23460  dvfsumlem4  23541  ftc1a  23549  ftc1lem6  23553  uc1pmon1p  23660  ig1pval2  23682  dgradd2  23773  dgrcolem2  23779  plydivlem4  23800  plydiveu  23802  elqaalem3  23825  qaa  23827  ulmdvlem1  23903  abelthlem6  23939  abelthlem7  23941  eflogeq  24097  jensenlem2  24459  harmonicbnd4  24482  sgmnncl  24618  dchrptlem2  24735  1lgs  24810  lgs1  24811  dchrisumlem2  24924  dchrisum0lem2a  24951  selberg2lem  24984  pntrsumo1  24999  pntrsumbnd  25000  pntpbnd1  25020  pntlemr  25036  pntlemj  25037  padicabvf  25065  istrkg3ld  25105  cusgraexilem2  25790  cusgraexi  25791  cusgrasizeinds  25798  wwlksubclwwlk  26126  erclwwlkref  26135  erclwwlknref  26147  eupacl  26290  eupapf  26293  eupaseg  26294  frgrancvvdeqlemC  26360  frghash2spot  26384  isgrpoi  26530  grpoinvfval  26554  grpodivfval  26566  vcz  26619  vcoprneOLD  26628  cnaddabloOLD  26632  nvz0  26729  sspz  26806  lno0  26829  nmobndi  26848  ipasslem2  26905  shunssi  27445  ococin  27485  ssjo  27524  pjocini  27775  nlfnval  27958  lncnopbd  28114  riesz3i  28139  cnlnadjlem7  28150  pjclem4  28276  pj3si  28284  hstoc  28299  hstnmoc  28300  hstoh  28309  hst0  28310  mdsl2i  28399  chirredlem3  28469  chirredlem4  28470  dmdbr5ati  28499  rexunirn  28549  fcnvgreu  28689  infxrge0glb  28754  2sqcoprm  28812  omndmul2  28877  omndmul  28879  isarchi3  28906  orng0le1  28977  esumcvg  29309  esumcvgre  29314  sigaval  29334  unelldsys  29382  fiunelros  29398  measval  29422  pmeasmono  29547  eulerpartlemgvv  29599  probfinmeasb  29652  ballotlemfc0  29715  ballotlemfcc  29716  ballotlemsi  29737  ballotlemfrci  29750  sgnneg  29763  signlem0  29824  bnj1006  30117  bnj1110  30138  bnj1253  30173  bnj1280  30176  bnj1463  30211  bnj1312  30214  erdszelem7  30267  erdszelem8  30268  cvmliftlem10  30364  cvmliftlem13  30366  cvmlift2lem9  30381  cvmlift3lem6  30394  cvmlift3lem7  30395  cvmlift3lem9  30397  dfrdg2  30779  dftrpred3g  30811  frrlem5  30862  bdayval  30879  cldregopn  31330  tailfval  31371  filnetlem3  31379  filnetlem4  31380  ontopbas  31431  bj-toponss  32065  f1omptsnlem  32183  icoreunrn  32207  relowlpssretop  32212  wl-sbal2  32350  unccur  32386  poimirlem1  32404  poimirlem2  32405  poimirlem4  32407  poimirlem6  32409  poimirlem7  32410  poimirlem11  32414  poimirlem12  32415  poimirlem17  32420  poimirlem20  32423  poimirlem22  32425  poimirlem23  32426  poimirlem28  32431  poimir  32436  ismblfin  32444  cnambfre  32452  bddiblnc  32474  ftc1cnnc  32478  dvasin  32490  ismtyres  32601  heiborlem8  32611  ghomidOLD  32682  rngolz  32715  rngorz  32716  rngosn6  32719  rngonegmn1l  32734  rngonegmn1r  32735  rngoneglmul  32736  rngonegrmul  32737  idlnegcl  32815  0idl  32818  0rngo  32820  keridl  32825  smprngopr  32845  lshpne0  33115  lkrval  33217  ldualvaddval  33260  ldualvsval  33267  opoc1  33331  pmap0  33893  pmap1N  33895  pexmidALTN  34106  cdleme31fv  34520  cdlemg27b  34826  erngdvlem4  35121  erng0g  35124  erngdvlem4-rN  35129  dvalveclem  35156  dvh0g  35242  dih0cnv  35414  dih1rn  35418  dih1cnv  35419  doch0  35489  doch1  35490  lcfl7lem  35630  mapdheq  35859  hdmap1eq  35933  hdmapval2lem  35965  hgmapvvlem3  36059  mzpval  36137  mzpindd  36151  pellex  36241  2nn0ind  36352  jm2.26lem3  36410  pw2f1o2val  36448  wepwsolem  36454  fnwe2lem3  36464  lnmfg  36494  dgrsub2  36548  mpaaeu  36563  flcidc  36587  rtrclexlem  36766  cnvrcl0  36775  brcoffn  37172  clsk1indlem3  37185  clsneif1o  37246  clsneicnv  37247  clsneikex  37248  clsneinex  37249  neicvgmex  37259  neicvgel1  37261  suprleubrd  37312  suprlubrd  37316  imo72b2  37321  dvconstbi  37379  bcc0  37385  binomcxplemnotnn0  37401  nnfoctb  38062  infleinflem1  38351  fprodcnlem  38490  sumnnodd  38521  icccncfext  38597  itgsin0pilem1  38665  stoweidlem22  38739  stoweidlem32  38749  stoweidlem35  38752  stoweidlem36  38753  stoweidlem37  38754  stoweidlem43  38760  stoweidlem50  38767  wallispilem5  38786  stirlinglem2  38792  stirlinglem3  38793  stirlinglem4  38794  stirlinglem8  38798  stirlinglem11  38801  stirlinglem12  38802  stirlinglem14  38804  stirlinglem15  38805  fourierdlem11  38835  fourierdlem20  38844  fourierdlem21  38845  fourierdlem41  38865  fourierdlem42  38866  fourierdlem48  38871  fourierdlem49  38872  fourierdlem64  38887  fourierdlem71  38894  fourierdlem79  38902  fourierdlem90  38913  fourierdlem91  38914  fourierswlem  38947  etransclem17  38968  etransclem38  38989  meaiininclem  39200  issmflelem  39455  issmfgtlem  39466  issmfgelem  39479  bgoldbtbndlem2  40047  bgoldbtbndlem3  40048  bgoldbtbnd  40050  pfxid  40080  pfx2  40100  structiedg0val  40277  incistruhgr  40327  uhgredgiedgb  40380  uhgriedg0edg0  40382  subgrprop3  40522  subgruhgredgd  40530  usgrexi  40683  cusgrexi  40684  cusgrsizeinds  40690  vtxduhgr0e  40715  vtxdgfusgrf  40734  1hevtxdg1  40743  1egrvtxdg1  40747  ewlkprop  40827  1wlklenvm1  40848  1wlkl1loop  40864  1wlkp1lem4  40907  2pthnloop  40959  upgrclwlkcompim  41010  crctcsh1wlkn0lem4  41038  crctcsh1wlkn0lem5  41039  crctcsh1wlkn0lem6  41040  crctcsh1wlkn0lem7  41041  crctcshlem4  41045  wspthnonp  41077  1wlkpwwlkf1ouspgr  41098  wwlksnwwlksnon  41143  2trld  41167  2spthd  41170  umgr2wlkon  41179  elwwlks2ons3  41181  elwspths2spth  41193  umgrclwwlksge2  41241  wwlksubclwwlks  41254  erclwwlksref  41263  erclwwlksnref  41275  0pthon1-av  41318  11wlkdlem4  41329  1trld  41331  1pthd  41332  3spthd  41365  3cycld  41367  eupth2eucrct  41407  eucrctshift  41433  eucrct2eupth  41435  frgrncvvdeqlemC  41500  frgrhash2wsp  41519  isclintop  41655  clintopcllaw  41659  nzrneg1ne0  41681  rnglz  41696  c0snmgmhm  41726  zrrnghm  41729  lidldomn1  41733  uzlidlring  41741  2zrngnmlid  41761  cznrng  41769  zrinitorngc  41814  zrtermorngc  41815  zrtermoringc  41884  coe1id  41988  blenre  42188  blennn  42189
  Copyright terms: Public domain W3C validator