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

Theorem adddii 11209
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 11177 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1485 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1563  wcel 2145  (class class class)co 7400  cc 11086   + caddc 11091   · cmul 11093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11155
This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103
This theorem is referenced by:  addrid  11378  3t3e9  12396  numltc  12730  numsucc  12744  numma  12748  decmul10add  12773  4t3lem  12801  9t11e99OLD  12835  decbin2  12847  binom2i  14236  3dec  14290  faclbnd4lem1  14317  3dvds2dec  16379  mod2xnegi  17119  decsplit  17130  log2ublem1  27065  log2ublem2  27066  bposlem8  27409  ax5seglem7  29190  ip0i  31082  ip1ilem  31083  ipasslem10  31096  normlem0  31366  polid2i  31414  lnopunilem1  32267  dfdec100  33082  dpmul10  33122  dpmul  33140  dpmul4  33141  cos9thpiminplylem5  34088  sn-1ne2  42887  sqmid3api  42899  ipiiie0  43054  sn-0tie0  43080  fourierswlem  46803  3exp4mod41  48224  2t6m3t4e0  48980
  Copyright terms: Public domain W3C validator