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

Theorem mpdan 683
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 584 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpidan  685  mpan2  687  mpjaodan  954  mpd3an3  1455  eueq2  3705  csbiegf  3920  difsnb  4738  reusv3i  5301  fimadmfo  6598  fimadmfoALT  6600  fvtresfn  6769  fvmpt3  6771  ffvelrnd  6850  fnressn  6918  fsnex  7035  f1oiso2  7099  riota5f  7136  onsucuni  7536  seqomlem2  8083  oaordi  8167  nnaordi  8239  qsdisj  8369  dom2lem  8543  canth2g  8665  limenpsi  8686  php4  8698  onfin  8703  sucxpdom  8721  xpfi  8783  dmfi  8796  pwfilem  8812  pwfi  8813  fiin  8880  supiso  8933  ordiso2  8973  wdom2d  9038  infeq5  9094  cantnfp1lem3  9137  cantnflem1d  9145  rankwflemb  9216  onenon  9372  cardonle  9380  sdomsdomcardi  9394  acni  9465  cardaleph  9509  djuen  9589  djuinf  9608  infdju1  9609  pwsdompw  9620  infdif  9625  cfval  9663  fin34  9806  fin1a2lem1  9816  fin1a2  9831  ttukeylem6  9930  sdomsdomcard  9976  canth3  9977  fpwwe2  10059  canthwelem  10066  gchdju1  10072  pwfseqlem4  10078  gchdjuidm  10084  gchxpidm  10085  tskwe2  10189  rankcf  10193  tskuni  10199  gruxp  10223  dmrecnq  10384  lterpq  10386  archnq  10396  reclem3pr  10465  reclem4pr  10466  0idsr  10513  lep1  11475  ledivp1  11536  negfi  11583  supaddc  11602  supmul1  11604  suprzcl  12056  uz11  12261  zmin  12338  zbtwnre  12340  rpnnen1lem4  12374  rpnnen1lem5  12375  xnegid  12626  supxrre  12715  infxrre  12724  eluzfz2  12910  fzsuc  12949  fzsuc2  12960  fzp1disj  12961  fzneuz  12983  nn0p1elfzo  13075  fllep1  13166  fraclt1  13167  fracle1  13168  fracge0  13169  flhalf  13195  ceige  13208  ceim1l  13210  fldiv  13223  modval  13234  suppssfz  13357  seqeq1  13367  expubnd  13536  iexpcyc  13564  binom2sub1  13577  faclbnd4lem3  13650  pfxid  14041  pfxccatpfx2  14094  swrdccat3blem  14096  cshw0  14151  cshwn  14154  cshimadifsn  14186  cshimadifsn0  14187  pfx2  14304  trclexlem  14349  shftfval  14424  shftcan1  14437  reval  14460  cjmulrcl  14498  addcj  14502  absval  14592  absneg  14632  abscj  14634  sqabsadd  14637  sqabssub  14638  leabs  14654  sqreulem  14714  lo1res  14911  o1of2  14964  o1rlimmul  14970  flo1  15204  trirecip  15213  efcan  15444  efi4p  15485  resin4p  15486  recos4p  15487  sincossq  15524  ruclem10  15587  iddvds  15618  1dvds  15619  2ebits  15791  lcmftp  15975  coprmgcdb  15988  1idssfct  16019  exprmfct  16043  eulerthlem2  16114  odzphi  16128  pcprendvds  16172  pcmpt  16223  oddprmdvds  16234  vdwlem8  16319  0ram2  16352  prmgaplem7  16388  setsn0fun  16515  setsexstruct2  16517  pwsvscaval  16763  2initoinv  17265  initoeu1  17266  initoeu2lem1  17269  initoeu2  17271  2termoinv  17272  termoeu1  17273  homarel  17291  joinfval  17606  meetfval  17620  latjcom  17664  latmcom  17680  0subm  17977  sgrp2nmndlem5  18039  grprcan  18082  isgrpid2  18085  grpinvid  18105  mulgnn0z  18199  0subg  18249  qus0  18283  ghmker  18329  symginv  18467  pmtrfrn  18522  odmulg2  18618  slwpgp  18674  pj1eq  18762  efgtf  18784  frgpinv  18826  frgpup2  18838  cnaddablx  18924  cnaddabl  18925  zaddablx  18928  dprdfadd  19078  dpjidcl  19116  dpjlid  19119  pgpfac1lem3  19135  srgen1zr  19216  1unit  19344  unitgrpid  19355  1rinv  19365  irredn0  19389  irredneg  19396  isdrng2  19448  rnrhmsubrg  19503  abv0  19538  abv1z  19539  abvneg  19541  lmodfopne  19608  lsssn0  19655  lspsn0  19716  lsp0  19717  lmhmvsca  19753  lmhmrnlss  19758  lmhmkerlss  19759  lsppratlem5  19859  rsp1  19932  ringen1zr  19985  rlmassa  20035  snifpsrbag  20081  psrvscaval  20107  psrdi  20121  psrdir  20122  mplvscaval  20163  mhpmpl  20270  mhpdeg  20271  coe1sclmulfv  20386  ply1idvr1  20396  evl1var  20434  cnfldneg  20506  zringcyg  20573  chrid  20609  chrrhm  20613  ip0r  20716  ocvlss  20751  ocv1  20758  mamuvs1  20949  mamuvs2  20950  matecl  20969  matvscacell  20980  mat0scmat  21082  submaval0  21124  mdetrsca  21147  maduval  21182  minmar1val0  21191  pmatcollpw3fi1lem2  21330  chcoeffeqlem  21428  cayleyhamilton0  21432  cayleyhamiltonALT  21434  toponsspwpw  21465  cctop  21549  cldval  21566  ntrfval  21567  clsfval  21568  cmclsopn  21605  opncldf3  21629  neifval  21642  lpfval  21681  cnrmnrm  21904  dis2ndc  22003  islocfin  22060  tx1cn  22152  idqtop  22249  kqtopon  22270  kqid  22271  kqcld  22278  hmphen2  22342  filssufil  22455  ufileu  22462  alexsublem  22587  symgtgp  22644  ustuqtop4  22787  cstucnd  22827  metustexhalf  23100  nm0  23172  rlmnlm  23231  nmolb  23260  metdseq0  23396  pi1xfrval  23592  clmvneg1  23637  clmvsubval  23647  ipcau2  23771  tcphcphlem1  23772  tcphcphlem2  23773  cmetcaulem  23825  ovolicc2lem3  24054  ovolicc2lem4  24055  mbfmulc2lem  24182  i1fpos  24241  mbfi1fseqlem3  24252  itg2ge0  24270  dvres2  24444  dvaddbr  24469  dvmulbr  24470  dvcobr  24477  dvfsumlem4  24560  ftc1a  24568  ftc1lem6  24572  uc1pmon1p  24679  ig1pval2  24701  dgradd2  24792  dgrcolem2  24798  plydivlem4  24819  plydiveu  24821  elqaalem3  24844  qaa  24846  ulmdvlem1  24922  abelthlem6  24958  abelthlem7  24960  eflogeq  25117  jensenlem2  25498  harmonicbnd4  25521  sgmnncl  25657  dchrptlem2  25774  1lgs  25849  lgs1  25850  2sqcoprm  25944  addsqnreup  25952  dchrisumlem2  25999  dchrisum0lem2a  26026  selberg2lem  26059  pntrsumo1  26074  pntrsumbnd  26075  pntpbnd1  26095  pntlemr  26111  pntlemj  26112  padicabvf  26140  incistruhgr  26797  subgrprop3  26991  subgruhgredgd  26999  usgrexi  27156  cusgrexi  27158  cusgrsizeinds  27167  vtxdgfusgrf  27212  1hevtxdg1  27221  1egrvtxdg1  27224  ewlkprop  27318  wlklenvm1  27336  wlkl1loop  27352  wlkp1lem4  27391  2pthnloop  27445  upgrclwlkcompim  27495  crctcshwlkn0lem4  27524  crctcshwlkn0lem5  27525  crctcshwlkn0lem6  27526  crctcshwlkn0lem7  27527  crctcshlem4  27531  wspthnonp  27570  wlkswwlksf1o  27590  wwlksnwwlksnon  27627  umgr2wlkon  27662  wwlks2onv  27665  elwwlks2ons3im  27666  elwspths2spth  27679  umgrclwwlkge2  27702  clwlkclwwlkf1lem3  27717  erclwwlkref  27731  clwwlknp  27748  wwlksext2clwwlk  27769  wwlksubclwwlk  27770  0pthon1  27840  1wlkdlem4  27852  1pthd  27855  3spthd  27888  eupth2eucrct  27929  eucrctshift  27955  eucrct2eupth  27957  frgrncvvdeqlem8  28018  frgr2wwlkeqm  28043  isgrpoi  28208  grpoinvfval  28232  grpodivfval  28244  vcz  28285  cnaddabloOLD  28291  nvz0  28378  sspz  28445  lno0  28466  nmobndi  28485  ipasslem2  28542  shunssi  29078  ococin  29118  ssjo  29157  pjocini  29408  nlfnval  29591  lncnopbd  29747  riesz3i  29772  cnlnadjlem7  29783  pjclem4  29909  pj3si  29917  hstoc  29932  hstnmoc  29933  hstoh  29942  hst0  29943  mdsl2i  30032  chirredlem3  30102  chirredlem4  30103  dmdbr5ati  30132  rexunirn  30189  fcnvgreu  30352  infxrge0glb  30421  omndmul2  30646  omndmul  30648  cycpmco2lem5  30705  cycpmco2lem6  30706  cycpmco2lem7  30707  isarchi3  30749  orng0le1  30818  fedgmullem1  30930  extdg1id  30958  esumcvg  31250  esumcvgre  31255  sigaval  31275  unelldsys  31322  fiunelros  31338  measval  31362  pmeasmono  31487  probfinmeasb  31591  ballotlemfc0  31655  ballotlemfcc  31656  ballotlemsi  31677  ballotlemfrci  31690  sgnneg  31703  signlem0  31762  breprexp  31809  bnj1006  32136  bnj1110  32157  bnj1253  32192  bnj1280  32195  bnj1463  32230  bnj1312  32233  erdszelem7  32347  erdszelem8  32348  cvmliftlem10  32444  cvmliftlem13  32446  cvmlift2lem9  32461  cvmlift3lem6  32474  cvmlift3lem7  32475  cvmlift3lem9  32477  satfv1lem  32512  dfrdg2  32943  dftrpred3g  32975  frpoinsg  32984  frrlem10  33035  bdayval  33058  noextendgt  33080  nosupbnd2lem1  33118  cldregopn  33582  tailfval  33623  filnetlem3  33631  filnetlem4  33632  ontopbas  33679  bj-elid4  34358  f1omptsnlem  34505  icoreunrn  34528  relowlpssretop  34533  fvineqsnf1  34579  wl-sbal2  34686  unccur  34761  poimirlem1  34779  poimirlem2  34780  poimirlem4  34782  poimirlem6  34784  poimirlem7  34785  poimirlem11  34789  poimirlem12  34790  poimirlem17  34795  poimirlem20  34798  poimirlem22  34800  poimirlem23  34801  poimirlem28  34806  poimir  34811  ismblfin  34819  cnambfre  34826  bddiblnc  34848  ftc1cnnc  34852  dvasin  34864  ismtyres  34973  heiborlem8  34983  ghomidOLD  35054  rngosn6  35091  rngonegmn1l  35106  rngonegmn1r  35107  rngoneglmul  35108  rngonegrmul  35109  idlnegcl  35187  0idl  35190  0rngo  35192  smprngopr  35217  cossex  35550  qsdisjALTV  35736  cnvepresdmqss  35772  lkrval  36110  ldualvaddval  36153  ldualvsval  36160  opoc1  36224  pmap0  36787  pmap1N  36789  pexmidALTN  37000  cdleme31fv  37412  cdlemg27b  37718  erngdvlem4  38013  erng0g  38016  erngdvlem4-rN  38021  dvalveclem  38047  dvh0g  38133  dih0cnv  38305  dih1rn  38309  dih1cnv  38310  doch0  38380  doch1  38381  lcfl7lem  38521  mapdheq  38750  hdmap1eq  38823  hdmapval2lem  38853  hgmapvvlem3  38947  frlmsnic  39033  renegid  39087  sn-0ne2  39120  remul01  39121  remulinvcom  39132  mzpval  39213  mzpindd  39227  pellex  39316  2nn0ind  39426  jm2.26lem3  39482  pw2f1o2val  39520  wepwsolem  39526  fnwe2lem3  39536  lnmfg  39566  dgrsub2  39619  mpaaeu  39634  flcidc  39658  rtrclexlem  39860  cnvrcl0  39869  brcoffn  40264  clsk1indlem3  40277  clsneif1o  40338  clsneicnv  40339  clsneikex  40340  clsneinex  40341  neicvgmex  40351  neicvgel1  40353  suprleubrd  40401  suprlubrd  40405  imo72b2  40410  dvconstbi  40550  bcc0  40556  binomcxplemnotnn0  40572  nnfoctb  41193  infleinflem1  41522  fprodcnlem  41764  sumnnodd  41795  icccncfext  42054  itgsin0pilem1  42119  stoweidlem32  42202  stoweidlem35  42205  stoweidlem36  42206  stoweidlem37  42207  stoweidlem43  42213  stoweidlem50  42220  wallispilem5  42239  stirlinglem2  42245  stirlinglem3  42246  stirlinglem4  42247  stirlinglem8  42251  stirlinglem11  42254  stirlinglem12  42255  stirlinglem14  42257  stirlinglem15  42258  fourierdlem11  42288  fourierdlem20  42297  fourierdlem21  42298  fourierdlem41  42318  fourierdlem42  42319  fourierdlem48  42324  fourierdlem49  42325  fourierdlem64  42340  fourierdlem71  42347  fourierdlem79  42355  fourierdlem90  42366  fourierdlem91  42367  fourierswlem  42400  etransclem17  42421  etransclem38  42442  saluni  42494  meaiininclem  42653  issmflelem  42906  issmfgtlem  42917  issmfgelem  42930  smflimsuplem4  42982  sprval  43492  prprval  43527  bgoldbtbndlem2  43822  bgoldbtbndlem3  43823  bgoldbtbnd  43825  isomushgr  43842  isomuspgrlem1  43843  efmndtmd  43971  isclintop  44016  clintopcllaw  44020  nzrneg1ne0  44042  c0snmgmhm  44087  zrrnghm  44090  lidldomn1  44094  zlidlring  44101  uzlidlring  44102  2zrngnmlid  44122  cznrng  44128  zrinitorngc  44173  zrtermorngc  44174  zrtermoringc  44243  coe1id  44340  blenre  44536  blennn  44537  ehl2eudisval0  44614  eenglngeehlnmlem2  44627  itsclc0yqsol  44653  inlinecirc02plem  44675
  Copyright terms: Public domain W3C validator