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

Theorem mpdan 702
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 693 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  mpidan  704  mpan2  707  mpjaodan  827  mpd3an3  1424  eueq2  3378  csbiegf  3555  difsnb  4335  reusv3i  4873  fvtresfn  6282  fvmpt3  6284  ffvelrnd  6358  fnressn  6422  fsnex  6535  f1oiso2  6599  riota5f  6633  onsucuni  7025  wfrlem5  7416  seqomlem2  7543  oaordi  7623  nnaordi  7695  qsdisj  7821  dom2lem  7992  canth2g  8111  limenpsi  8132  php4  8144  onfin  8148  sucxpdom  8166  xpfi  8228  dmfi  8241  pwfilem  8257  pwfi  8258  fiin  8325  supiso  8378  ordiso2  8417  wdom2d  8482  infeq5  8531  cantnfp1lem3  8574  cantnflem1d  8582  rankwflemb  8653  onenon  8772  cardonle  8780  sdomsdomcardi  8794  acni  8865  cardaleph  8909  cdaen  8992  cdainf  9011  infcda1  9012  pwsdompw  9023  infdif  9028  cfval  9066  fin34  9209  fin1a2lem1  9219  fin1a2  9234  ttukeylem6  9333  sdomsdomcard  9379  canth3  9380  fpwwe2  9462  canthwelem  9469  gchcda1  9475  pwfseqlem4  9481  gchcdaidm  9487  gchxpidm  9488  tskwe2  9592  rankcf  9596  tskuni  9602  gruxp  9626  dmrecnq  9787  lterpq  9789  archnq  9799  reclem3pr  9868  reclem4pr  9869  0idsr  9915  lep1  10859  ledivp1  10922  negfi  10968  supaddc  10987  supmul1  10989  suprzcl  11454  uz11  11707  zmin  11781  zbtwnre  11783  rpnnen1lem4  11814  rpnnen1lem5  11815  rpnnen1lem4OLD  11820  rpnnen1lem5OLD  11821  xnegid  12066  xrsupss  12136  xrinfmss  12137  supxrre  12154  infxrre  12163  eluzfz2  12346  fzsuc  12385  fzsuc2  12395  fzp1disj  12396  fzneuz  12417  nn0p1elfzo  12506  fllep1  12597  fraclt1  12598  fracle1  12599  fracge0  12600  flhalf  12626  ceige  12639  ceim1l  12641  fldiv  12654  modval  12665  suppssfz  12789  seqeq1  12799  expubnd  12916  iexpcyc  12964  binom2sub1  12977  faclbnd4lem3  13077  swrdid  13422  swrdccat3blem  13489  cshwn  13537  cshimadifsn  13569  cshimadifsn0  13570  trclexlem  13727  shftfval  13804  shftcan1  13817  reval  13840  cjmulrcl  13878  addcj  13882  absval  13972  absneg  14011  abscj  14013  sqabsadd  14016  sqabssub  14017  leabs  14033  sqreulem  14093  lo1res  14284  o1of2  14337  o1rlimmul  14343  flo1  14580  trirecip  14589  efcan  14820  efi4p  14861  resin4p  14862  recos4p  14863  sincossq  14900  ruclem10  14962  iddvds  14989  1dvds  14990  2ebits  15163  lcmftp  15343  coprmgcdb  15356  1idssfct  15387  exprmfct  15410  eulerthlem2  15481  odzphi  15495  pcprendvds  15539  pcmpt  15590  vdwlem8  15686  0ram2  15719  prmgaplem7  15755  setsn0fun  15889  setsexstruct2  15891  pwsvscaval  16149  issect2  16408  2initoinv  16654  initoeu1  16655  initoeu2lem1  16658  initoeu2  16660  2termoinv  16661  termoeu1  16662  homarel  16680  joinfval  16995  meetfval  17009  latjcom  17053  latmcom  17069  sgrp2nmndlem5  17410  grprcan  17449  isgrpid2  17452  grpinvid  17470  mulgnn0z  17561  0subg  17613  qus0  17646  ghmker  17680  symginv  17816  pmtrfrn  17872  odmulg2  17966  slwpgp  18022  pj1eq  18107  efgtf  18129  frgpinv  18171  frgpup2  18183  mulgnn0di  18225  cnaddablx  18265  cnaddabl  18266  zaddablx  18269  dprdfadd  18413  dpjidcl  18451  dpjlid  18454  pgpfac1lem3  18470  srgen1zr  18524  ringlz  18581  ringrz  18582  1unit  18652  unitgrpid  18663  1rinv  18673  irredn0  18697  irredneg  18704  isdrng2  18751  abv0  18825  abv1z  18826  abvneg  18828  lmodfopne  18895  lsssn0  18942  lspsn0  19002  lsp0  19003  lmhmvsca  19039  lmhmrnlss  19044  lmhmkerlss  19045  lsppratlem5  19145  rsp1  19218  ringen1zr  19271  rlmassa  19320  snifpsrbag  19360  psrvscaval  19386  psrdi  19400  psrdir  19401  mplsubglem  19428  mplvscaval  19442  coe1sclmulfv  19647  ply1idvr1  19657  evl1var  19694  cnfldneg  19766  zringcyg  19833  chrid  19869  chrrhm  19873  ip0r  19976  ocvlss  20010  ocv1  20017  mamuvs1  20205  mamuvs2  20206  matecl  20225  matvscacell  20236  mat0scmat  20338  submaval0  20380  mdetrsca  20403  maduval  20438  minmar1val0  20447  pmatcollpw3fi1lem2  20586  chfacfscmulgsum  20659  chfacfpmmulgsum  20663  chcoeffeqlem  20684  cayleyhamilton0  20688  cayleyhamiltonALT  20690  toponsspwpw  20720  cctop  20804  cldval  20821  ntrfval  20822  clsfval  20823  cmclsopn  20860  opncldf3  20884  neifval  20897  lpfval  20936  cnrmnrm  21159  islocfin  21314  tx1cn  21406  idqtop  21503  kqtopon  21524  kqid  21525  kqcld  21532  hmphen2  21596  filssufil  21710  ufileu  21717  alexsublem  21842  symgtgp  21899  ustuqtop4  22042  cstucnd  22082  metustexhalf  22355  nm0  22427  rlmnlm  22486  nmolb  22515  metdseq0  22651  pi1xfrval  22848  clmvneg1  22893  clmvsubval  22903  ipcau2  23027  tchcphlem1  23028  tchcphlem2  23029  cmetcaulem  23080  ovolicc2lem3  23281  ovolicc2lem4  23282  mbfmulc2lem  23408  i1fpos  23467  mbfi1fseqlem3  23478  mbfi1fseqlem4  23479  itg2ge0  23496  dvres2  23670  dvaddbr  23695  dvmulbr  23696  dvcobr  23703  dvfsumlem4  23786  ftc1a  23794  ftc1lem6  23798  uc1pmon1p  23905  ig1pval2  23927  dgradd2  24018  dgrcolem2  24024  plydivlem4  24045  plydiveu  24047  elqaalem3  24070  qaa  24072  ulmdvlem1  24148  abelthlem6  24184  abelthlem7  24186  eflogeq  24342  jensenlem2  24708  harmonicbnd4  24731  sgmnncl  24867  dchrptlem2  24984  1lgs  25059  lgs1  25060  dchrisumlem2  25173  dchrisum0lem2a  25200  selberg2lem  25233  pntrsumo1  25248  pntrsumbnd  25249  pntpbnd1  25269  pntlemr  25285  pntlemj  25286  padicabvf  25314  istrkg3ld  25354  incistruhgr  25968  subgrprop3  26162  subgruhgredgd  26170  usgrexi  26331  cusgrexi  26333  cusgrsizeinds  26342  vtxdgfusgrf  26387  1hevtxdg1  26396  1egrvtxdg1  26399  ewlkprop  26493  wlklenvm1  26511  wlkl1loop  26528  wlkp1lem4  26567  2pthnloop  26621  upgrclwlkcompim  26671  crctcshwlkn0lem4  26699  crctcshwlkn0lem5  26700  crctcshwlkn0lem6  26701  crctcshwlkn0lem7  26702  crctcshlem4  26706  wspthnonp  26738  wlkpwwlkf1ouspgr  26759  wwlksnwwlksnon  26804  umgr2wlkon  26840  elwwlks2ons3  26842  elwspths2spth  26856  umgrclwwlksge2  26905  wwlksubclwwlks  26918  erclwwlksref  26927  erclwwlksnref  26939  0pthon1  26982  1wlkdlem4  26993  1pthd  26996  3spthd  27029  eupth2eucrct  27070  eucrctshift  27096  eucrct2eupth  27098  frgrncvvdeqlem8  27163  frgr2wwlkeqm  27182  isgrpoi  27336  grpoinvfval  27360  grpodivfval  27372  vcz  27414  cnaddabloOLD  27420  nvz0  27507  sspz  27574  lno0  27595  nmobndi  27614  ipasslem2  27671  shunssi  28211  ococin  28251  ssjo  28290  pjocini  28541  nlfnval  28724  lncnopbd  28880  riesz3i  28905  cnlnadjlem7  28916  pjclem4  29042  pj3si  29050  hstoc  29065  hstnmoc  29066  hstoh  29075  hst0  29076  mdsl2i  29165  chirredlem3  29235  chirredlem4  29236  dmdbr5ati  29265  rexunirn  29315  fcnvgreu  29457  infxrge0glb  29515  2sqcoprm  29632  omndmul2  29697  omndmul  29699  isarchi3  29726  orng0le1  29797  esumcvg  30133  esumcvgre  30138  sigaval  30158  unelldsys  30206  fiunelros  30222  measval  30246  pmeasmono  30371  eulerpartlemgvv  30423  probfinmeasb  30476  ballotlemfc0  30539  ballotlemfcc  30540  ballotlemsi  30561  ballotlemfrci  30574  sgnneg  30587  signlem0  30649  breprexp  30696  bnj1006  31014  bnj1110  31035  bnj1253  31070  bnj1280  31073  bnj1463  31108  bnj1312  31111  erdszelem7  31164  erdszelem8  31165  cvmliftlem10  31261  cvmliftlem13  31263  cvmlift2lem9  31278  cvmlift3lem6  31291  cvmlift3lem7  31292  cvmlift3lem9  31294  dfrdg2  31685  dftrpred3g  31717  frrlem5  31768  bdayval  31785  noextendgt  31807  nosupbnd2lem1  31845  cldregopn  32310  tailfval  32351  filnetlem3  32359  filnetlem4  32360  ontopbas  32411  f1omptsnlem  33163  icoreunrn  33187  relowlpssretop  33192  wl-sbal2  33327  unccur  33372  poimirlem1  33390  poimirlem2  33391  poimirlem4  33393  poimirlem6  33395  poimirlem7  33396  poimirlem11  33400  poimirlem12  33401  poimirlem17  33406  poimirlem20  33409  poimirlem22  33411  poimirlem23  33412  poimirlem28  33417  poimir  33422  ismblfin  33430  cnambfre  33438  bddiblnc  33460  ftc1cnnc  33464  dvasin  33476  ismtyres  33587  heiborlem8  33597  ghomidOLD  33668  rngolz  33701  rngorz  33702  rngosn6  33705  rngonegmn1l  33720  rngonegmn1r  33721  rngoneglmul  33722  rngonegrmul  33723  idlnegcl  33801  0idl  33804  0rngo  33806  keridl  33811  smprngopr  33831  lshpne0  34099  lkrval  34201  ldualvaddval  34244  ldualvsval  34251  opoc1  34315  pmap0  34877  pmap1N  34879  pexmidALTN  35090  cdleme31fv  35504  cdlemg27b  35810  erngdvlem4  36105  erng0g  36108  erngdvlem4-rN  36113  dvalveclem  36140  dvh0g  36226  dih0cnv  36398  dih1rn  36402  dih1cnv  36403  doch0  36473  doch1  36474  lcfl7lem  36614  mapdheq  36843  hdmap1eq  36917  hdmapval2lem  36949  hgmapvvlem3  37043  mzpval  37121  mzpindd  37135  pellex  37225  2nn0ind  37336  jm2.26lem3  37394  pw2f1o2val  37432  wepwsolem  37438  fnwe2lem3  37448  lnmfg  37478  dgrsub2  37531  mpaaeu  37546  flcidc  37570  rtrclexlem  37749  cnvrcl0  37758  brcoffn  38154  clsk1indlem3  38167  clsneif1o  38228  clsneicnv  38229  clsneikex  38230  clsneinex  38231  neicvgmex  38241  neicvgel1  38243  suprleubrd  38292  suprlubrd  38296  imo72b2  38301  dvconstbi  38359  bcc0  38365  binomcxplemnotnn0  38381  nnfoctb  39039  infleinflem1  39405  fprodcnlem  39637  sumnnodd  39668  icccncfext  39869  itgsin0pilem1  39934  stoweidlem22  40008  stoweidlem32  40018  stoweidlem35  40021  stoweidlem36  40022  stoweidlem37  40023  stoweidlem43  40029  stoweidlem50  40036  wallispilem5  40055  stirlinglem2  40061  stirlinglem3  40062  stirlinglem4  40063  stirlinglem8  40067  stirlinglem11  40070  stirlinglem12  40071  stirlinglem14  40073  stirlinglem15  40074  fourierdlem11  40104  fourierdlem20  40113  fourierdlem21  40114  fourierdlem41  40134  fourierdlem42  40135  fourierdlem48  40140  fourierdlem49  40141  fourierdlem64  40156  fourierdlem71  40163  fourierdlem79  40171  fourierdlem90  40182  fourierdlem91  40183  fourierswlem  40216  etransclem17  40237  etransclem38  40258  saluni  40313  meaiininclem  40469  issmflelem  40722  issmfgtlem  40733  issmfgelem  40746  smflimsuplem4  40798  pfxid  41163  pfx2  41183  bgoldbtbndlem2  41465  bgoldbtbndlem3  41466  bgoldbtbnd  41468  sprval  41500  isclintop  41614  clintopcllaw  41618  nzrneg1ne0  41640  rnglz  41655  c0snmgmhm  41685  zrrnghm  41688  lidldomn1  41692  uzlidlring  41700  2zrngnmlid  41720  cznrng  41726  zrinitorngc  41771  zrtermorngc  41772  zrtermoringc  41841  coe1id  41943  blenre  42139  blennn  42140  onsetreclem2  42220
  Copyright terms: Public domain W3C validator