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  12399  numltc  12733  numsucc  12747  numma  12751  decmul10add  12776  4t3lem  12804  9t11e99OLD  12838  decbin2  12850  binom2i  14239  3dec  14293  faclbnd4lem1  14320  3dvds2dec  16381  mod2xnegi  17121  decsplit  17132  log2ublem1  27069  log2ublem2  27070  bposlem8  27413  ax5seglem7  29194  ip0i  31086  ip1ilem  31087  ipasslem10  31100  normlem0  31370  polid2i  31418  lnopunilem1  32271  dfdec100  33087  dpmul10  33127  dpmul  33145  dpmul4  33146  cos9thpiminplylem5  34093  sn-1ne2  42892  sqmid3api  42904  ipiiie0  43059  sn-0tie0  43085  fourierswlem  46802  3exp4mod41  48223  2t6m3t4e0  48979
  Copyright terms: Public domain W3C validator