Theorem adddii 11223

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110   · cmul 11112

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090

This theorem is referenced by:  addrid  11391  3t3e9  12376  numltc  12700  numsucc  12714  numma  12718  decmul10add  12743  4t3lem  12771  9t11e99  12804  decbin2  12815  binom2i  14173  3dec  14223  faclbnd4lem1  14250  3dvds2dec  16273  mod2xnegi  17001  decsplit  17013  log2ublem1  26441  log2ublem2  26442  bposlem8  26784  ax5seglem7  28183  ip0i  30066  ip1ilem  30067  ipasslem10  30080  normlem0  30350  polid2i  30398  lnopunilem1  31251  dfdec100  32024  dpmul10  32049  dpmul  32067  dpmul4  32068  sn-1ne2  41177  sqmid3api  41193  ipiiie0  41307  sn-0tie0  41309  fourierswlem  44933  3exp4mod41  46271  2t6m3t4e0  46978