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

Theorem adddii 10918
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 10891 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1459 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2108  (class class class)co 7255  cc 10800   + caddc 10805   · cmul 10807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10869
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087
This theorem is referenced by:  addid1  11085  3t3e9  12070  numltc  12392  numsucc  12406  numma  12410  decmul10add  12435  4t3lem  12463  9t11e99  12496  decbin2  12507  binom2i  13856  3dec  13908  faclbnd4lem1  13935  3dvds2dec  15970  mod2xnegi  16700  decsplit  16712  log2ublem1  26001  log2ublem2  26002  bposlem8  26344  ax5seglem7  27206  ip0i  29088  ip1ilem  29089  ipasslem10  29102  normlem0  29372  polid2i  29420  lnopunilem1  30273  dfdec100  31046  dpmul10  31071  dpmul  31089  dpmul4  31090  sn-1ne2  40216  sqmid3api  40232  ipiiie0  40340  sn-0tie0  40342  fourierswlem  43661  3exp4mod41  44956  2t6m3t4e0  45572
  Copyright terms: Public domain W3C validator