Theorem adddii 11186

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   · cmul 11073

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

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

This theorem is referenced by:  addrid  11354  3t3e9  12348  numltc  12675  numsucc  12689  numma  12693  decmul10add  12718  4t3lem  12746  9t11e99  12779  decbin2  12790  binom2i  14177  3dec  14231  faclbnd4lem1  14258  3dvds2dec  16303  mod2xnegi  17042  decsplit  17053  log2ublem1  26856  log2ublem2  26857  bposlem8  27202  ax5seglem7  28862  ip0i  30754  ip1ilem  30755  ipasslem10  30768  normlem0  31038  polid2i  31086  lnopunilem1  31939  dfdec100  32755  dpmul10  32815  dpmul  32833  dpmul4  32834  cos9thpiminplylem5  33776  sn-1ne2  42253  sqmid3api  42271  ipiiie0  42426  sn-0tie0  42439  fourierswlem  46228  3exp4mod41  47617  2t6m3t4e0  48336