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

Theorem mpdan 659
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 565 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 197  df-an 383
This theorem is referenced by:  mpidan  661  mpan2  663  mpjaodan  939  mpd3an3  1572  eueq2  3530  csbiegf  3704  difsnb  4470  reusv3i  5003  fvtresfn  6426  fvmpt3  6428  ffvelrnd  6503  fnressn  6567  fsnex  6680  f1oiso2  6744  riota5f  6778  onsucuni  7174  wfrlem5  7571  seqomlem2  7698  oaordi  7779  nnaordi  7851  qsdisj  7975  dom2lem  8148  canth2g  8269  limenpsi  8290  php4  8302  onfin  8306  sucxpdom  8324  xpfi  8386  dmfi  8399  pwfilem  8415  pwfi  8416  fiin  8483  supiso  8536  ordiso2  8575  wdom2d  8640  infeq5  8697  cantnfp1lem3  8740  cantnflem1d  8748  rankwflemb  8819  onenon  8974  cardonle  8982  sdomsdomcardi  8996  acni  9067  cardaleph  9111  cdaen  9196  cdainf  9215  infcda1  9216  pwsdompw  9227  infdif  9232  cfval  9270  fin34  9413  fin1a2lem1  9423  fin1a2  9438  ttukeylem6  9537  sdomsdomcard  9583  canth3  9584  fpwwe2  9666  canthwelem  9673  gchcda1  9679  pwfseqlem4  9685  gchcdaidm  9691  gchxpidm  9692  tskwe2  9796  rankcf  9800  tskuni  9806  gruxp  9830  dmrecnq  9991  lterpq  9993  archnq  10003  reclem3pr  10072  reclem4pr  10073  0idsr  10119  lep1  11063  ledivp1  11126  negfi  11172  supaddc  11191  supmul1  11193  suprzcl  11658  uz11  11910  zmin  11986  zbtwnre  11988  rpnnen1lem4  12019  rpnnen1lem5  12020  rpnnen1lem4OLD  12025  rpnnen1lem5OLD  12026  xnegid  12273  xrsupss  12343  xrinfmss  12344  supxrre  12361  infxrre  12370  eluzfz2  12555  fzsuc  12594  fzsuc2  12604  fzp1disj  12605  fzneuz  12627  nn0p1elfzo  12718  fllep1  12809  fraclt1  12810  fracle1  12811  fracge0  12812  flhalf  12838  ceige  12851  ceim1l  12853  fldiv  12866  modval  12877  suppssfz  13000  seqeq1  13010  expubnd  13127  iexpcyc  13175  binom2sub1  13188  faclbnd4lem3  13285  swrdid  13636  swrdccat3blem  13703  cshwn  13751  cshimadifsn  13783  cshimadifsn0  13784  trclexlem  13942  shftfval  14017  shftcan1  14030  reval  14053  cjmulrcl  14091  addcj  14095  absval  14185  absneg  14224  abscj  14226  sqabsadd  14229  sqabssub  14230  leabs  14246  sqreulem  14306  lo1res  14497  o1of2  14550  o1rlimmul  14556  flo1  14792  trirecip  14801  efcan  15031  efi4p  15072  resin4p  15073  recos4p  15074  sincossq  15111  ruclem10  15173  iddvds  15203  1dvds  15204  2ebits  15376  lcmftp  15556  coprmgcdb  15569  1idssfct  15599  exprmfct  15622  eulerthlem2  15693  odzphi  15707  pcprendvds  15751  pcmpt  15802  vdwlem8  15898  0ram2  15931  prmgaplem7  15967  setsn0fun  16101  setsexstruct2  16103  pwsvscaval  16362  issect2  16620  2initoinv  16866  initoeu1  16867  initoeu2lem1  16870  initoeu2  16872  2termoinv  16873  termoeu1  16874  homarel  16892  joinfval  17208  meetfval  17222  latjcom  17266  latmcom  17282  sgrp2nmndlem5  17623  grprcan  17662  isgrpid2  17665  grpinvid  17683  mulgnn0z  17774  0subg  17826  qus0  17859  ghmker  17893  symginv  18028  pmtrfrn  18084  odmulg2  18178  slwpgp  18234  pj1eq  18319  efgtf  18341  frgpinv  18383  frgpup2  18395  mulgnn0di  18437  cnaddablx  18477  cnaddabl  18478  zaddablx  18481  dprdfadd  18626  dpjidcl  18664  dpjlid  18667  pgpfac1lem3  18683  srgen1zr  18737  ringlz  18794  ringrz  18795  1unit  18865  unitgrpid  18876  1rinv  18886  irredn0  18910  irredneg  18917  isdrng2  18966  abv0  19040  abv1z  19041  abvneg  19043  lmodfopne  19110  lsssn0  19157  lspsn0  19220  lsp0  19221  lmhmvsca  19257  lmhmrnlss  19262  lmhmkerlss  19263  lsppratlem5  19365  rsp1  19438  ringen1zr  19491  rlmassa  19540  snifpsrbag  19580  psrvscaval  19606  psrdi  19620  psrdir  19621  mplsubglem  19648  mplvscaval  19662  coe1sclmulfv  19867  ply1idvr1  19877  evl1var  19914  cnfldneg  19986  zringcyg  20053  chrid  20089  chrrhm  20093  ip0r  20198  ocvlss  20232  ocv1  20239  mamuvs1  20427  mamuvs2  20428  matecl  20447  matvscacell  20458  mat0scmat  20561  submaval0  20603  mdetrsca  20626  maduval  20661  minmar1val0  20670  pmatcollpw3fi1lem2  20811  chfacfscmulgsum  20884  chfacfpmmulgsum  20888  chcoeffeqlem  20909  cayleyhamilton0  20913  cayleyhamiltonALT  20915  toponsspwpw  20946  cctop  21030  cldval  21047  ntrfval  21048  clsfval  21049  cmclsopn  21086  opncldf3  21110  neifval  21123  lpfval  21162  cnrmnrm  21385  islocfin  21540  tx1cn  21632  idqtop  21729  kqtopon  21750  kqid  21751  kqcld  21758  hmphen2  21822  filssufil  21935  ufileu  21942  alexsublem  22067  symgtgp  22124  ustuqtop4  22267  cstucnd  22307  metustexhalf  22580  nm0  22652  rlmnlm  22711  nmolb  22740  metdseq0  22876  pi1xfrval  23072  clmvneg1  23117  clmvsubval  23127  ipcau2  23251  tchcphlem1  23252  tchcphlem2  23253  cmetcaulem  23304  ovolicc2lem3  23506  ovolicc2lem4  23507  mbfmulc2lem  23633  i1fpos  23692  mbfi1fseqlem3  23703  mbfi1fseqlem4  23704  itg2ge0  23721  dvres2  23895  dvaddbr  23920  dvmulbr  23921  dvcobr  23928  dvfsumlem4  24011  ftc1a  24019  ftc1lem6  24023  uc1pmon1p  24130  ig1pval2  24152  dgradd2  24243  dgrcolem2  24249  plydivlem4  24270  plydiveu  24272  elqaalem3  24295  qaa  24297  ulmdvlem1  24373  abelthlem6  24409  abelthlem7  24411  eflogeq  24568  jensenlem2  24934  harmonicbnd4  24957  sgmnncl  25093  dchrptlem2  25210  1lgs  25285  lgs1  25286  dchrisumlem2  25399  dchrisum0lem2a  25426  selberg2lem  25459  pntrsumo1  25474  pntrsumbnd  25475  pntpbnd1  25495  pntlemr  25511  pntlemj  25512  padicabvf  25540  istrkg3ld  25580  incistruhgr  26194  subgrprop3  26390  subgruhgredgd  26398  usgrexi  26571  cusgrexi  26573  cusgrsizeinds  26582  vtxdgfusgrf  26627  1hevtxdg1  26636  1egrvtxdg1  26639  ewlkprop  26733  wlklenvm1  26751  wlkl1loop  26768  wlkp1lem4  26807  2pthnloop  26861  upgrclwlkcompim  26911  crctcshwlkn0lem4  26940  crctcshwlkn0lem5  26941  crctcshwlkn0lem6  26942  crctcshwlkn0lem7  26943  crctcshlem4  26947  wspthnonp  26992  wlkpwwlkf1ouspgr  27012  wwlksnwwlksnon  27057  wwlksnwwlksnonOLD  27059  umgr2wlkon  27094  wwlks2onv  27097  elwwlks2ons3im  27098  elwwlks2ons3OLD  27100  elwspths2spth  27113  umgrclwwlkge2  27138  clwlkclwwlkf1lem3  27153  erclwwlkref  27167  clwwlknp  27189  wwlksext2clwwlk  27211  wwlksubclwwlk  27213  0pthon1  27305  1wlkdlem4  27317  1pthd  27320  3spthd  27353  eupth2eucrct  27394  eucrctshift  27420  eucrct2eupth  27422  frgrncvvdeqlem8  27485  frgr2wwlkeqm  27510  isgrpoi  27686  grpoinvfval  27710  grpodivfval  27722  vcz  27764  cnaddabloOLD  27770  nvz0  27857  sspz  27924  lno0  27945  nmobndi  27964  ipasslem2  28021  shunssi  28561  ococin  28601  ssjo  28640  pjocini  28891  nlfnval  29074  lncnopbd  29230  riesz3i  29255  cnlnadjlem7  29266  pjclem4  29392  pj3si  29400  hstoc  29415  hstnmoc  29416  hstoh  29425  hst0  29426  mdsl2i  29515  chirredlem3  29585  chirredlem4  29586  dmdbr5ati  29615  rexunirn  29664  fcnvgreu  29806  infxrge0glb  29864  2sqcoprm  29981  omndmul2  30046  omndmul  30048  isarchi3  30075  orng0le1  30146  esumcvg  30482  esumcvgre  30487  sigaval  30507  unelldsys  30555  fiunelros  30571  measval  30595  pmeasmono  30720  eulerpartlemgvv  30772  probfinmeasb  30825  ballotlemfc0  30888  ballotlemfcc  30889  ballotlemsi  30910  ballotlemfrci  30923  sgnneg  30936  signlem0  30998  breprexp  31045  bnj1006  31361  bnj1110  31382  bnj1253  31417  bnj1280  31420  bnj1463  31455  bnj1312  31458  erdszelem7  31511  erdszelem8  31512  cvmliftlem10  31608  cvmliftlem13  31610  cvmlift2lem9  31625  cvmlift3lem6  31638  cvmlift3lem7  31639  cvmlift3lem9  31641  dfrdg2  32031  dftrpred3g  32063  frpoinsg  32072  frrlem5  32115  bdayval  32132  noextendgt  32154  nosupbnd2lem1  32192  cldregopn  32657  tailfval  32698  filnetlem3  32706  filnetlem4  32707  ontopbas  32758  f1omptsnlem  33513  icoreunrn  33537  relowlpssretop  33542  wl-sbal2  33674  unccur  33718  poimirlem1  33736  poimirlem2  33737  poimirlem4  33739  poimirlem6  33741  poimirlem7  33742  poimirlem11  33746  poimirlem12  33747  poimirlem17  33752  poimirlem20  33755  poimirlem22  33757  poimirlem23  33758  poimirlem28  33763  poimir  33768  ismblfin  33776  cnambfre  33783  bddiblnc  33805  ftc1cnnc  33809  dvasin  33821  ismtyres  33932  heiborlem8  33942  ghomidOLD  34013  rngolz  34046  rngorz  34047  rngosn6  34050  rngonegmn1l  34065  rngonegmn1r  34066  rngoneglmul  34067  rngonegrmul  34068  idlnegcl  34146  0idl  34149  0rngo  34151  keridl  34156  smprngopr  34176  cossex  34509  lkrval  34890  ldualvaddval  34933  ldualvsval  34940  opoc1  35004  pmap0  35566  pmap1N  35568  pexmidALTN  35779  cdleme31fv  36192  cdlemg27b  36498  erngdvlem4  36793  erng0g  36796  erngdvlem4-rN  36801  dvalveclem  36828  dvh0g  36914  dih0cnv  37086  dih1rn  37090  dih1cnv  37091  doch0  37161  doch1  37162  lcfl7lem  37302  mapdheq  37531  hdmap1eq  37604  hdmapval2lem  37634  hgmapvvlem3  37728  mzpval  37814  mzpindd  37828  pellex  37918  2nn0ind  38029  jm2.26lem3  38087  pw2f1o2val  38125  wepwsolem  38131  fnwe2lem3  38141  lnmfg  38171  dgrsub2  38224  mpaaeu  38239  flcidc  38263  rtrclexlem  38442  cnvrcl0  38451  brcoffn  38847  clsk1indlem3  38860  clsneif1o  38921  clsneicnv  38922  clsneikex  38923  clsneinex  38924  neicvgmex  38934  neicvgel1  38936  suprleubrd  38985  suprlubrd  38989  imo72b2  38994  dvconstbi  39052  bcc0  39058  binomcxplemnotnn0  39074  nnfoctb  39728  infleinflem1  40096  fprodcnlem  40343  sumnnodd  40374  icccncfext  40612  itgsin0pilem1  40677  stoweidlem22  40750  stoweidlem32  40760  stoweidlem35  40763  stoweidlem36  40764  stoweidlem37  40765  stoweidlem43  40771  stoweidlem50  40778  wallispilem5  40797  stirlinglem2  40803  stirlinglem3  40804  stirlinglem4  40805  stirlinglem8  40809  stirlinglem11  40812  stirlinglem12  40813  stirlinglem14  40815  stirlinglem15  40816  fourierdlem11  40846  fourierdlem20  40855  fourierdlem21  40856  fourierdlem41  40876  fourierdlem42  40877  fourierdlem48  40882  fourierdlem49  40883  fourierdlem64  40898  fourierdlem71  40905  fourierdlem79  40913  fourierdlem90  40924  fourierdlem91  40925  fourierswlem  40958  etransclem17  40979  etransclem38  41000  saluni  41055  meaiininclem  41214  issmflelem  41467  issmfgtlem  41478  issmfgelem  41491  smflimsuplem4  41543  pfxid  41910  pfx2  41930  bgoldbtbndlem2  42212  bgoldbtbndlem3  42213  bgoldbtbnd  42215  sprval  42247  isclintop  42361  clintopcllaw  42365  nzrneg1ne0  42387  rnglz  42402  c0snmgmhm  42432  zrrnghm  42435  lidldomn1  42439  uzlidlring  42447  2zrngnmlid  42467  cznrng  42473  zrinitorngc  42518  zrtermorngc  42519  zrtermoringc  42588  coe1id  42690  blenre  42886  blennn  42887  onsetreclem2  42970
  Copyright terms: Public domain W3C validator