Theorem adddii 11247

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 11218	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	mp3an 1463	1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   + caddc 11132   · cmul 11134

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

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

This theorem is referenced by:  addrid  11415  3t3e9  12407  numltc  12734  numsucc  12748  numma  12752  decmul10add  12777  4t3lem  12805  9t11e99  12838  decbin2  12849  binom2i  14230  3dec  14284  faclbnd4lem1  14311  3dvds2dec  16352  mod2xnegi  17091  decsplit  17102  log2ublem1  26908  log2ublem2  26909  bposlem8  27254  ax5seglem7  28914  ip0i  30806  ip1ilem  30807  ipasslem10  30820  normlem0  31090  polid2i  31138  lnopunilem1  31991  dfdec100  32809  dpmul10  32869  dpmul  32887  dpmul4  32888  cos9thpiminplylem5  33820  sn-1ne2  42315  sqmid3api  42333  ipiiie0  42480  sn-0tie0  42482  fourierswlem  46259  3exp4mod41  47630  2t6m3t4e0  48323