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

Theorem mpdan 668
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 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpan2  671  mpjaodan  786  mpd3an3  1325  eueq2  3273  csbiegf  3458  difsnb  4172  reusv3i  4659  fvtresfn  5957  fvmpt3  5959  ffvelrnd  6032  fnressn  6083  f1oiso2  6248  riota5f  6282  onsucuni  6663  seqomlem2  7135  oaordi  7214  nnaordi  7286  qsdisj  7407  dom2lem  7575  canth2g  7691  limenpsi  7712  php4  7724  onfin  7728  sucxpdom  7749  xpfi  7811  dmfi  7823  pwfilem  7834  pwfi  7835  fiin  7902  supiso  7954  ordiso2  7961  wdom2d  8027  infeq5  8075  cantnfp1lem3  8120  cantnflem1d  8128  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  rankwflemb  8232  onenon  8351  cardonle  8359  sdomsdomcardi  8373  acni  8447  cardaleph  8491  cdaen  8574  cdainf  8593  infcda1  8594  pwsdompw  8605  infdif  8610  cfval  8648  fin34  8791  fin1a2lem1  8801  fin1a2  8816  ttukeylem6  8915  sdomsdomcard  8956  canth3  8957  fpwwe2  9042  canthwelem  9049  gchcda1  9055  pwfseqlem4  9061  gchcdaidm  9067  gchxpidm  9068  tskwe2  9172  rankcf  9176  tskuni  9182  gruxp  9206  dmrecnq  9367  lterpq  9369  archnq  9379  reclem3pr  9448  reclem4pr  9449  0idsr  9495  lep1  10406  ledivp1  10472  supmul1  10533  suprzcl  10967  uz11  11132  zmin  11207  zbtwnre  11209  rpnnen1lem4  11240  rpnnen1lem5  11241  xnegid  11464  xrsupss  11529  xrinfmss  11530  supxrre  11548  infmxrre  11556  eluzfz2  11723  fzsuc  11756  fzsuc2  11766  fzp1disj  11767  fzneuz  11788  fllep1  11938  fraclt1  11939  fracle1  11940  fracge0  11941  flhalf  11962  ceige  11972  ceim1l  11974  fldiv  11987  modval  11998  suppssfz  12100  seqeq1  12110  expubnd  12226  iexpcyc  12272  faclbnd4lem3  12373  faclbnd4lem4  12374  swrdccat3blem  12720  cshwn  12768  shftfval  12903  shftcan1  12916  reval  12939  cjmulrcl  12977  addcj  12981  absval  13071  absneg  13110  abscj  13112  sqabsadd  13115  sqabssub  13116  leabs  13132  sqreulem  13192  lo1res  13382  o1of2  13435  o1rlimmul  13441  sumrb  13535  flo1  13666  trirecip  13674  prodrblem2  13738  efcan  13831  efi4p  13872  resin4p  13873  recos4p  13874  sincossq  13911  ruclem10  13972  iddvds  13997  1dvds  13998  2ebits  14097  1idssfct  14223  exprmfct  14251  eulerthlem2  14312  odzphi  14323  pcprendvds  14364  pcmpt  14411  vdwlem8  14506  0ram2  14539  pwsvscaval  14892  issect2  15149  homarel  15363  joinfval  15631  meetfval  15645  latjcom  15689  latmcom  15705  sgrp2nmndlem5  16047  grprcan  16083  isgrpid2  16086  grpinvid  16101  mulgnn0z  16162  0subg  16226  qus0  16259  ghmker  16292  symginv  16427  pmtrfrn  16483  odmulg2  16577  slwpgp  16633  pj1eq  16718  efgtf  16740  frgpinv  16782  frgpup2  16794  mulgnn0di  16834  cnaddablx  16874  cnaddabl  16875  zaddablx  16876  dprdfadd  17060  dprdfaddOLD  17067  dpjidcl  17107  dpjlid  17110  dpjidclOLD  17114  pgpfac1lem3  17128  srgen1zr  17181  ringlz  17235  ringrz  17236  1unit  17307  unitgrpid  17318  1rinv  17328  irredn0  17352  irredneg  17359  isdrng2  17406  abv0  17480  abv1z  17481  abvneg  17483  lsssn0  17594  lspsn0  17654  lsp0  17655  lmhmvsca  17691  lmhmrnlss  17696  lmhmkerlss  17697  lsppratlem5  17797  rsp1  17872  ringen1zr  17925  rlmassa  17975  asclpropd  17995  snifpsrbag  18015  psrvscaval  18045  psrdi  18061  psrdir  18062  mplsubglem  18093  mplsubglemOLD  18095  mplvscaval  18110  coe1sclmulfv  18324  ply1idvr1  18334  evl1var  18372  cnfldneg  18444  zringcyg  18513  zcyg  18518  chrid  18564  chrrhm  18568  ip0r  18672  ocvlss  18703  ocv1  18710  mamuvs1  18907  mamuvs2  18908  matecl  18927  matvscacell  18938  mat0scmat  19040  submaval0  19082  mdetrsca  19105  maduval  19140  minmar1val0  19149  pmatcollpw3fi1lem2  19288  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chcoeffeqlem  19386  cayleyhamilton0  19390  cayleyhamiltonALT  19392  cctop  19507  cldval  19524  ntrfval  19525  clsfval  19526  cmclsopn  19563  opncldf3  19587  neifval  19600  lpfval  19639  cnrmnrm  19862  islocfin  20018  tx1cn  20110  tx2cn  20111  idqtop  20207  kqtopon  20228  kqid  20229  kqcld  20236  hmphen2  20300  filssufil  20413  ufileu  20420  alexsublem  20544  symgtgp  20600  ustuqtop4  20747  ustuqtop5  20748  cstucnd  20787  metustexhalfOLD  21066  metustexhalf  21067  nm0  21146  rlmnlm  21197  nmolb  21224  metdseq0  21358  iocopnst  21440  pi1xfrval  21554  clmvneg1  21591  ipcau2  21677  tchcphlem1  21678  tchcphlem2  21679  cmetcaulem  21727  ovolicc2lem3  21930  ovolicc2lem4  21931  mbfmulc2lem  22054  i1fpos  22113  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  itg2ge0  22142  dvres2  22316  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvfsumlem4  22430  ftc1a  22438  ftc1lem6  22442  uc1pmon1p  22552  ig1pval2  22574  dgradd2  22665  dgrcolem2  22671  plydivlem4  22692  plydiveu  22694  elqaalem3  22717  qaa  22719  ulmdvlem1  22795  abelthlem6  22831  abelthlem7  22833  eflogeq  22986  jensenlem2  23317  harmonicbnd4  23340  sgmnncl  23421  dchrptlem2  23540  1lgs  23612  lgs1  23613  dchrisumlem2  23675  dchrisum0lem2a  23702  selberg2lem  23735  pntrsumo1  23750  pntrsumbnd  23751  pntpbnd1  23771  pntlemr  23787  pntlemj  23788  padicabvf  23816  tglineeltr  24011  cusgraexilem2  24467  cusgraexi  24468  cusgrasizeinds  24476  wwlksubclwwlk  24804  erclwwlkref  24813  erclwwlknref  24825  eupacl  24969  eupapf  24972  eupaseg  24973  frgrancvvdeqlemC  25039  frghash2spot  25063  isgrpoi  25200  grpoinvfval  25226  grpoinvid  25234  grpodivfval  25244  gxfval  25259  gxid  25275  issubgo  25305  cnaddablo  25352  ghomidOLD  25367  rngolz  25403  rngorz  25404  rngosn6  25430  vcz  25463  vcoprne  25472  nvz0  25571  sspz  25648  lno0  25671  nmobndi  25690  ipasslem2  25747  shunssi  26286  ococin  26326  ssjo  26365  pjocini  26616  nlfnval  26800  lncnopbd  26956  riesz3i  26981  cnlnadjlem7  26992  pjclem4  27118  pj3si  27126  hstoc  27141  hstnmoc  27142  hstoh  27151  hst0  27152  mdsl2i  27241  chirredlem3  27311  chirredlem4  27312  dmdbr5ati  27341  rexunirn  27390  fcnvgreu  27514  2sqcoprm  27635  omndmul2  27702  omndmul  27704  isarchi3  27731  orng0le1  27802  esumcvg  28092  sigaval  28110  measval  28169  eulerpartlemgvv  28315  probfinmeasb  28368  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsi  28453  ballotlemfrci  28466  sgnneg  28479  signlem0  28544  erdszelem7  28641  erdszelem8  28642  cvmliftlem10  28739  cvmliftlem13  28741  cvmlift2lem9  28756  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  ghomgrpilem2  29026  dfrdg2  29228  dftrpred3g  29316  wfrlem5  29347  frrlem5  29391  bdayval  29408  ontopbas  29893  wl-sbal2  30014  supaddc  30041  ismblfin  30055  cnambfre  30063  bddiblnc  30085  ftc1cnnc  30089  dvasin  30103  cldregopn  30149  tailfval  30190  filnetlem3  30198  filnetlem4  30199  ismtyres  30304  heiborlem8  30314  rngonegmn1l  30352  rngonegmn1r  30353  rngoneglmul  30354  rngonegrmul  30355  idlnegcl  30419  0idl  30422  0rngo  30424  keridl  30429  smprngopr  30449  mzpval  30664  mzpindd  30678  pellex  30771  2nn0ind  30881  jm2.26lem3  30943  pw2f1o2val  30981  wepwsolem  30987  fnwe2lem3  30998  lnmfg  31028  dgrsub2  31084  mpaaeu  31099  flcidc  31123  dvconstbi  31239  bcc0  31245  binomcxplemnotnn0  31261  sumnnodd  31636  icccncfext  31690  itgsin0pilem1  31748  stoweidlem22  31804  stoweidlem32  31814  stoweidlem35  31817  stoweidlem36  31818  stoweidlem37  31819  stoweidlem43  31825  stoweidlem50  31832  wallispilem5  31851  stirlinglem2  31857  stirlinglem3  31858  stirlinglem4  31859  stirlinglem8  31863  stirlinglem11  31866  stirlinglem12  31867  stirlinglem14  31869  stirlinglem15  31870  fourierdlem11  31900  fourierdlem20  31909  fourierdlem21  31910  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem64  31953  fourierdlem71  31960  fourierdlem79  31968  fourierdlem90  31979  fourierdlem91  31980  fourierswlem  32013  etransclem17  32034  etransclem38  32055  usgrauvtxvd  32358  vdcusgra  32359  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  isclintop  32531  clintopcllaw  32535  2initoinv  32616  initoeu1  32617  initoeu2lem1  32620  initoeu2  32622  2termoinv  32623  termoeu1  32624  nzrneg1ne0  32675  rnglz  32690  c0snmgmhm  32720  zrrnghm  32723  lidldomn1  32727  uzlidlring  32735  2zrngnmlid  32755  cznrng  32763  zrinitorngc  32808  zrtermorngc  32809  zrtermoringc  32878  coe1id  32984  bnj1006  34017  bnj1110  34038  bnj1253  34073  bnj1280  34076  bnj1463  34111  bnj1312  34114  lshpne0  34711  lkrval  34813  ldualvaddval  34856  ldualvsval  34863  opoc1  34927  pmap0  35489  pmap1N  35491  pexmidALTN  35702  cdleme31fv  36116  cdlemg27b  36422  erngdvlem4  36717  erng0g  36720  erngdvlem4-rN  36725  dvalveclem  36752  dvh0g  36838  dih0cnv  37010  dih1rn  37014  dih1cnv  37015  doch0  37085  doch1  37086  lcfl7lem  37226  mapdheq  37455  hdmap1eq  37529  hdmapval2lem  37561  hgmapvvlem3  37655  suprleubrd  37983  suprlubrd  37987  imo72b2  37993
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 185  df-an 371
  Copyright terms: Public domain W3C validator