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

Theorem adddii 11256
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 11227 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1458 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  wcel 2099  (class class class)co 7420  cc 11136   + caddc 11141   · cmul 11143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11205
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087
This theorem is referenced by:  addrid  11424  3t3e9  12409  numltc  12733  numsucc  12747  numma  12751  decmul10add  12776  4t3lem  12804  9t11e99  12837  decbin2  12848  binom2i  14207  3dec  14257  faclbnd4lem1  14284  3dvds2dec  16309  mod2xnegi  17039  decsplit  17051  log2ublem1  26877  log2ublem2  26878  bposlem8  27223  ax5seglem7  28745  ip0i  30634  ip1ilem  30635  ipasslem10  30648  normlem0  30918  polid2i  30966  lnopunilem1  31819  dfdec100  32593  dpmul10  32618  dpmul  32636  dpmul4  32637  sn-1ne2  41840  sqmid3api  41857  ipiiie0  41992  sn-0tie0  41994  fourierswlem  45618  3exp4mod41  46956  2t6m3t4e0  47412
  Copyright terms: Public domain W3C validator