Theorem adddii 11131

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016   · cmul 11018

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

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

This theorem is referenced by:  addrid  11300  3t3e9  12294  numltc  12620  numsucc  12634  numma  12638  decmul10add  12663  4t3lem  12691  9t11e99  12724  decbin2  12735  binom2i  14121  3dec  14175  faclbnd4lem1  14202  3dvds2dec  16246  mod2xnegi  16985  decsplit  16996  log2ublem1  26884  log2ublem2  26885  bposlem8  27230  ax5seglem7  28915  ip0i  30807  ip1ilem  30808  ipasslem10  30821  normlem0  31091  polid2i  31139  lnopunilem1  31992  dfdec100  32818  dpmul10  32882  dpmul  32900  dpmul4  32901  cos9thpiminplylem5  33820  sn-1ne2  42384  sqmid3api  42402  ipiiie0  42557  sn-0tie0  42570  fourierswlem  46353  3exp4mod41  47741  2t6m3t4e0  48473