Theorem adddii 11146

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

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		adddi 11117	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	mp3an 1463	1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11314  3t3e9  12308  numltc  12635  numsucc  12649  numma  12653  decmul10add  12678  4t3lem  12706  9t11e99  12739  decbin2  12750  binom2i  14137  3dec  14191  faclbnd4lem1  14218  3dvds2dec  16262  mod2xnegi  17001  decsplit  17012  log2ublem1  26872  log2ublem2  26873  bposlem8  27218  ax5seglem7  28898  ip0i  30787  ip1ilem  30788  ipasslem10  30801  normlem0  31071  polid2i  31119  lnopunilem1  31972  dfdec100  32788  dpmul10  32848  dpmul  32866  dpmul4  32867  cos9thpiminplylem5  33752  sn-1ne2  42238  sqmid3api  42256  ipiiie0  42411  sn-0tie0  42424  fourierswlem  46212  3exp4mod41  47601  2t6m3t4e0  48333