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

Theorem adddii 11226
Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 ๐ด โˆˆ โ„‚
axi.2 ๐ต โˆˆ โ„‚
axi.3 ๐ถ โˆˆ โ„‚
Assertion
Ref Expression
adddii (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))

Proof of Theorem adddii
StepHypRef Expression
1 axi.1 . 2 ๐ด โˆˆ โ„‚
2 axi.2 . 2 ๐ต โˆˆ โ„‚
3 axi.3 . 2 ๐ถ โˆˆ โ„‚
4 adddi 11199 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
51, 2, 3, 4mp3an 1462 1 (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7409  โ„‚cc 11108   + caddc 11113   ยท cmul 11115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11177
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090
This theorem is referenced by:  addrid  11394  3t3e9  12379  numltc  12703  numsucc  12717  numma  12721  decmul10add  12746  4t3lem  12774  9t11e99  12807  decbin2  12818  binom2i  14176  3dec  14226  faclbnd4lem1  14253  3dvds2dec  16276  mod2xnegi  17004  decsplit  17016  log2ublem1  26451  log2ublem2  26452  bposlem8  26794  ax5seglem7  28193  ip0i  30078  ip1ilem  30079  ipasslem10  30092  normlem0  30362  polid2i  30410  lnopunilem1  31263  dfdec100  32036  dpmul10  32061  dpmul  32079  dpmul4  32080  sn-1ne2  41179  sqmid3api  41195  ipiiie0  41310  sn-0tie0  41312  fourierswlem  44946  3exp4mod41  46284  2t6m3t4e0  47024
  Copyright terms: Public domain W3C validator