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

Theorem adddii 10630
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 10603 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1458 1 (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  (class class class)co 7130  cc 10512   + caddc 10517   · cmul 10519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10581
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  addid1  10797  3t3e9  11782  numltc  12102  numsucc  12116  numma  12120  decmul10add  12145  4t3lem  12173  9t11e99  12206  decbin2  12217  binom2i  13558  3dec  13610  faclbnd4lem1  13637  3dvds2dec  15661  mod2xnegi  16384  decsplit  16396  log2ublem1  25510  log2ublem2  25511  bposlem8  25853  ax5seglem7  26707  ip0i  28586  ip1ilem  28587  ipasslem10  28600  normlem0  28870  polid2i  28918  lnopunilem1  29771  dfdec100  30532  dpmul10  30557  dpmul  30575  dpmul4  30576  sn-1ne2  39280  sqmid3api  39291  fourierswlem  42663  3exp4mod41  43926  2t6m3t4e0  44541
  Copyright terms: Public domain W3C validator