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

Theorem mpdan 703
 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 694 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  mpidan  705  mpan2  707  mpjaodan  844  mpd3an3  1465  eueq2  3413  csbiegf  3590  difsnb  4369  reusv3i  4905  fvtresfn  6323  fvmpt3  6325  ffvelrnd  6400  fnressn  6465  fsnex  6578  f1oiso2  6642  riota5f  6676  onsucuni  7070  wfrlem5  7464  seqomlem2  7591  oaordi  7671  nnaordi  7743  qsdisj  7867  dom2lem  8037  canth2g  8155  limenpsi  8176  php4  8188  onfin  8192  sucxpdom  8210  xpfi  8272  dmfi  8285  pwfilem  8301  pwfi  8302  fiin  8369  supiso  8422  ordiso2  8461  wdom2d  8526  infeq5  8572  cantnfp1lem3  8615  cantnflem1d  8623  rankwflemb  8694  onenon  8813  cardonle  8821  sdomsdomcardi  8835  acni  8906  cardaleph  8950  cdaen  9033  cdainf  9052  infcda1  9053  pwsdompw  9064  infdif  9069  cfval  9107  fin34  9250  fin1a2lem1  9260  fin1a2  9275  ttukeylem6  9374  sdomsdomcard  9420  canth3  9421  fpwwe2  9503  canthwelem  9510  gchcda1  9516  pwfseqlem4  9522  gchcdaidm  9528  gchxpidm  9529  tskwe2  9633  rankcf  9637  tskuni  9643  gruxp  9667  dmrecnq  9828  lterpq  9830  archnq  9840  reclem3pr  9909  reclem4pr  9910  0idsr  9956  lep1  10900  ledivp1  10963  negfi  11009  supaddc  11028  supmul1  11030  suprzcl  11495  uz11  11748  zmin  11822  zbtwnre  11824  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  xnegid  12107  xrsupss  12177  xrinfmss  12178  supxrre  12195  infxrre  12204  eluzfz2  12387  fzsuc  12426  fzsuc2  12436  fzp1disj  12437  fzneuz  12459  nn0p1elfzo  12550  fllep1  12642  fraclt1  12643  fracle1  12644  fracge0  12645  flhalf  12671  ceige  12684  ceim1l  12686  fldiv  12699  modval  12710  suppssfz  12834  seqeq1  12844  expubnd  12961  iexpcyc  13009  binom2sub1  13022  faclbnd4lem3  13122  swrdid  13474  swrdccat3blem  13541  cshwn  13589  cshimadifsn  13621  cshimadifsn0  13622  trclexlem  13779  shftfval  13854  shftcan1  13867  reval  13890  cjmulrcl  13928  addcj  13932  absval  14022  absneg  14061  abscj  14063  sqabsadd  14066  sqabssub  14067  leabs  14083  sqreulem  14143  lo1res  14334  o1of2  14387  o1rlimmul  14393  flo1  14630  trirecip  14639  efcan  14870  efi4p  14911  resin4p  14912  recos4p  14913  sincossq  14950  ruclem10  15012  iddvds  15042  1dvds  15043  2ebits  15216  lcmftp  15396  coprmgcdb  15409  1idssfct  15440  exprmfct  15463  eulerthlem2  15534  odzphi  15548  pcprendvds  15592  pcmpt  15643  vdwlem8  15739  0ram2  15772  prmgaplem7  15808  setsn0fun  15942  setsexstruct2  15944  pwsvscaval  16202  issect2  16461  2initoinv  16707  initoeu1  16708  initoeu2lem1  16711  initoeu2  16713  2termoinv  16714  termoeu1  16715  homarel  16733  joinfval  17048  meetfval  17062  latjcom  17106  latmcom  17122  sgrp2nmndlem5  17463  grprcan  17502  isgrpid2  17505  grpinvid  17523  mulgnn0z  17614  0subg  17666  qus0  17699  ghmker  17733  symginv  17868  pmtrfrn  17924  odmulg2  18018  slwpgp  18074  pj1eq  18159  efgtf  18181  frgpinv  18223  frgpup2  18235  mulgnn0di  18277  cnaddablx  18317  cnaddabl  18318  zaddablx  18321  dprdfadd  18465  dpjidcl  18503  dpjlid  18506  pgpfac1lem3  18522  srgen1zr  18576  ringlz  18633  ringrz  18634  1unit  18704  unitgrpid  18715  1rinv  18725  irredn0  18749  irredneg  18756  isdrng2  18805  abv0  18879  abv1z  18880  abvneg  18882  lmodfopne  18949  lsssn0  18996  lspsn0  19056  lsp0  19057  lmhmvsca  19093  lmhmrnlss  19098  lmhmkerlss  19099  lsppratlem5  19199  rsp1  19272  ringen1zr  19325  rlmassa  19374  snifpsrbag  19414  psrvscaval  19440  psrdi  19454  psrdir  19455  mplsubglem  19482  mplvscaval  19496  coe1sclmulfv  19701  ply1idvr1  19711  evl1var  19748  cnfldneg  19820  zringcyg  19887  chrid  19923  chrrhm  19927  ip0r  20030  ocvlss  20064  ocv1  20071  mamuvs1  20259  mamuvs2  20260  matecl  20279  matvscacell  20290  mat0scmat  20392  submaval0  20434  mdetrsca  20457  maduval  20492  minmar1val0  20501  pmatcollpw3fi1lem2  20640  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  chcoeffeqlem  20738  cayleyhamilton0  20742  cayleyhamiltonALT  20744  toponsspwpw  20774  cctop  20858  cldval  20875  ntrfval  20876  clsfval  20877  cmclsopn  20914  opncldf3  20938  neifval  20951  lpfval  20990  cnrmnrm  21213  islocfin  21368  tx1cn  21460  idqtop  21557  kqtopon  21578  kqid  21579  kqcld  21586  hmphen2  21650  filssufil  21763  ufileu  21770  alexsublem  21895  symgtgp  21952  ustuqtop4  22095  cstucnd  22135  metustexhalf  22408  nm0  22480  rlmnlm  22539  nmolb  22568  metdseq0  22704  pi1xfrval  22900  clmvneg1  22945  clmvsubval  22955  ipcau2  23079  tchcphlem1  23080  tchcphlem2  23081  cmetcaulem  23132  ovolicc2lem3  23333  ovolicc2lem4  23334  mbfmulc2lem  23459  i1fpos  23518  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  itg2ge0  23547  dvres2  23721  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvfsumlem4  23837  ftc1a  23845  ftc1lem6  23849  uc1pmon1p  23956  ig1pval2  23978  dgradd2  24069  dgrcolem2  24075  plydivlem4  24096  plydiveu  24098  elqaalem3  24121  qaa  24123  ulmdvlem1  24199  abelthlem6  24235  abelthlem7  24237  eflogeq  24393  jensenlem2  24759  harmonicbnd4  24782  sgmnncl  24918  dchrptlem2  25035  1lgs  25110  lgs1  25111  dchrisumlem2  25224  dchrisum0lem2a  25251  selberg2lem  25284  pntrsumo1  25299  pntrsumbnd  25300  pntpbnd1  25320  pntlemr  25336  pntlemj  25337  padicabvf  25365  istrkg3ld  25405  incistruhgr  26019  subgrprop3  26213  subgruhgredgd  26221  usgrexi  26393  cusgrexi  26395  cusgrsizeinds  26404  vtxdgfusgrf  26449  1hevtxdg1  26458  1egrvtxdg1  26461  ewlkprop  26555  wlklenvm1  26573  wlkl1loop  26590  wlkp1lem4  26629  2pthnloop  26683  upgrclwlkcompim  26733  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  crctcshwlkn0lem7  26764  crctcshlem4  26768  wspthnonp  26813  wlkpwwlkf1ouspgr  26833  wwlksnwwlksnon  26878  wwlksnwwlksnonOLD  26880  umgr2wlkon  26915  wwlks2onv  26918  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  elwspths2spth  26934  umgrclwwlkge2  26957  erclwwlkref  26977  clwwlknp  26999  wwlksext2clwwlk  27021  wwlksubclwwlk  27023  0pthon1  27106  1wlkdlem4  27118  1pthd  27121  3spthd  27154  eupth2eucrct  27195  eucrctshift  27221  eucrct2eupth  27223  frgrncvvdeqlem8  27286  frgr2wwlkeqm  27311  isgrpoi  27480  grpoinvfval  27504  grpodivfval  27516  vcz  27558  cnaddabloOLD  27564  nvz0  27651  sspz  27718  lno0  27739  nmobndi  27758  ipasslem2  27815  shunssi  28355  ococin  28395  ssjo  28434  pjocini  28685  nlfnval  28868  lncnopbd  29024  riesz3i  29049  cnlnadjlem7  29060  pjclem4  29186  pj3si  29194  hstoc  29209  hstnmoc  29210  hstoh  29219  hst0  29220  mdsl2i  29309  chirredlem3  29379  chirredlem4  29380  dmdbr5ati  29409  rexunirn  29458  fcnvgreu  29600  infxrge0glb  29658  2sqcoprm  29775  omndmul2  29840  omndmul  29842  isarchi3  29869  orng0le1  29940  esumcvg  30276  esumcvgre  30281  sigaval  30301  unelldsys  30349  fiunelros  30365  measval  30389  pmeasmono  30514  eulerpartlemgvv  30566  probfinmeasb  30619  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsi  30704  ballotlemfrci  30717  sgnneg  30730  signlem0  30792  breprexp  30839  bnj1006  31155  bnj1110  31176  bnj1253  31211  bnj1280  31214  bnj1463  31249  bnj1312  31252  erdszelem7  31305  erdszelem8  31306  cvmliftlem10  31402  cvmliftlem13  31404  cvmlift2lem9  31419  cvmlift3lem6  31432  cvmlift3lem7  31433  cvmlift3lem9  31435  dfrdg2  31825  dftrpred3g  31857  frpoinsg  31866  frrlem5  31909  bdayval  31926  noextendgt  31948  nosupbnd2lem1  31986  cldregopn  32451  tailfval  32492  filnetlem3  32500  filnetlem4  32501  ontopbas  32552  f1omptsnlem  33313  icoreunrn  33337  relowlpssretop  33342  wl-sbal2  33477  unccur  33522  poimirlem1  33540  poimirlem2  33541  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem11  33550  poimirlem12  33551  poimirlem17  33556  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem28  33567  poimir  33572  ismblfin  33580  cnambfre  33588  bddiblnc  33610  ftc1cnnc  33614  dvasin  33626  ismtyres  33737  heiborlem8  33747  ghomidOLD  33818  rngolz  33851  rngorz  33852  rngosn6  33855  rngonegmn1l  33870  rngonegmn1r  33871  rngoneglmul  33872  rngonegrmul  33873  idlnegcl  33951  0idl  33954  0rngo  33956  keridl  33961  smprngopr  33981  cossex  34314  lshpne0  34591  lkrval  34693  ldualvaddval  34736  ldualvsval  34743  opoc1  34807  pmap0  35369  pmap1N  35371  pexmidALTN  35582  cdleme31fv  35995  cdlemg27b  36301  erngdvlem4  36596  erng0g  36599  erngdvlem4-rN  36604  dvalveclem  36631  dvh0g  36717  dih0cnv  36889  dih1rn  36893  dih1cnv  36894  doch0  36964  doch1  36965  lcfl7lem  37105  mapdheq  37334  hdmap1eq  37408  hdmapval2lem  37440  hgmapvvlem3  37534  mzpval  37612  mzpindd  37626  pellex  37716  2nn0ind  37827  jm2.26lem3  37885  pw2f1o2val  37923  wepwsolem  37929  fnwe2lem3  37939  lnmfg  37969  dgrsub2  38022  mpaaeu  38037  flcidc  38061  rtrclexlem  38240  cnvrcl0  38249  brcoffn  38645  clsk1indlem3  38658  clsneif1o  38719  clsneicnv  38720  clsneikex  38721  clsneinex  38722  neicvgmex  38732  neicvgel1  38734  suprleubrd  38783  suprlubrd  38787  imo72b2  38792  dvconstbi  38850  bcc0  38856  binomcxplemnotnn0  38872  nnfoctb  39527  infleinflem1  39899  fprodcnlem  40149  sumnnodd  40180  icccncfext  40418  itgsin0pilem1  40483  stoweidlem22  40557  stoweidlem32  40567  stoweidlem35  40570  stoweidlem36  40571  stoweidlem37  40572  stoweidlem43  40578  stoweidlem50  40585  wallispilem5  40604  stirlinglem2  40610  stirlinglem3  40611  stirlinglem4  40612  stirlinglem8  40616  stirlinglem11  40619  stirlinglem12  40620  stirlinglem14  40622  stirlinglem15  40623  fourierdlem11  40653  fourierdlem20  40662  fourierdlem21  40663  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem64  40705  fourierdlem71  40712  fourierdlem79  40720  fourierdlem90  40731  fourierdlem91  40732  fourierswlem  40765  etransclem17  40786  etransclem38  40807  saluni  40862  meaiininclem  41021  issmflelem  41274  issmfgtlem  41285  issmfgelem  41298  smflimsuplem4  41350  pfxid  41717  pfx2  41737  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  sprval  42054  isclintop  42168  clintopcllaw  42172  nzrneg1ne0  42194  rnglz  42209  c0snmgmhm  42239  zrrnghm  42242  lidldomn1  42246  uzlidlring  42254  2zrngnmlid  42274  cznrng  42280  zrinitorngc  42325  zrtermorngc  42326  zrtermoringc  42395  coe1id  42497  blenre  42693  blennn  42694  onsetreclem2  42777
 Copyright terms: Public domain W3C validator