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

Theorem adddii 11273
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 11244 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1463 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  (class class class)co 7431  cc 11153   + caddc 11158   · cmul 11160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11222
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089
This theorem is referenced by:  addrid  11441  3t3e9  12433  numltc  12759  numsucc  12773  numma  12777  decmul10add  12802  4t3lem  12830  9t11e99  12863  decbin2  12874  binom2i  14251  3dec  14305  faclbnd4lem1  14332  3dvds2dec  16370  mod2xnegi  17109  decsplit  17120  log2ublem1  26989  log2ublem2  26990  bposlem8  27335  ax5seglem7  28950  ip0i  30844  ip1ilem  30845  ipasslem10  30858  normlem0  31128  polid2i  31176  lnopunilem1  32029  dfdec100  32832  dpmul10  32877  dpmul  32895  dpmul4  32896  sn-1ne2  42300  sqmid3api  42318  ipiiie0  42467  sn-0tie0  42469  fourierswlem  46245  3exp4mod41  47603  2t6m3t4e0  48264
  Copyright terms: Public domain W3C validator