Theorem adddii 10642

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  addid1  10809  3t3e9  11792  numltc  12112  numsucc  12126  numma  12130  decmul10add  12155  4t3lem  12183  9t11e99  12216  decbin2  12227  binom2i  13570  3dec  13622  faclbnd4lem1  13649  3dvds2dec  15674  mod2xnegi  16397  decsplit  16409  log2ublem1  25532  log2ublem2  25533  bposlem8  25875  ax5seglem7  26729  ip0i  28608  ip1ilem  28609  ipasslem10  28622  normlem0  28892  polid2i  28940  lnopunilem1  29793  dfdec100  30572  dpmul10  30597  dpmul  30615  dpmul4  30616  sn-1ne2  39466  sqmid3api  39477  ipiiie0  39574  sn-0tie0  39576  fourierswlem  42872  3exp4mod41  44134  2t6m3t4e0  44750