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

Theorem adddii 10213
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 10188 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1561 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  wcel 2127  (class class class)co 6801  cc 10097   + caddc 10102   · cmul 10104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10166
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  addid1  10379  3t3e9  11343  numltc  11691  numsucc  11712  numma  11720  decmul10add  11756  decmul10addOLD  11757  4t3lem  11794  9t11e99  11834  9t11e99OLD  11835  decbin2  11846  binom2i  13139  3dec  13215  3decOLD  13218  faclbnd4lem1  13245  3dvds2dec  15229  3dvds2decOLD  15230  mod2xnegi  15948  decsplit  15960  decsplitOLD  15964  log2ublem1  24843  log2ublem2  24844  bposlem8  25186  ax5seglem7  25985  ip0i  27960  ip1ilem  27961  ipasslem10  27974  normlem0  28246  polid2i  28294  lnopunilem1  29149  dfdec100  29856  dpmul10  29883  dpmul  29901  dpmul4  29902  fourierswlem  40919  3exp4mod41  42012  2t6m3t4e0  42605
  Copyright terms: Public domain W3C validator