Theorem adddii 11156

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   · cmul 11043

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

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

This theorem is referenced by:  addrid  11325  3t3e9  12319  numltc  12645  numsucc  12659  numma  12663  decmul10add  12688  4t3lem  12716  9t11e99  12749  decbin2  12760  binom2i  14147  3dec  14201  faclbnd4lem1  14228  3dvds2dec  16272  mod2xnegi  17011  decsplit  17022  log2ublem1  26924  log2ublem2  26925  bposlem8  27270  ax5seglem7  29020  ip0i  30912  ip1ilem  30913  ipasslem10  30926  normlem0  31196  polid2i  31244  lnopunilem1  32097  dfdec100  32921  dpmul10  32986  dpmul  33004  dpmul4  33005  cos9thpiminplylem5  33963  sn-1ne2  42629  sqmid3api  42647  ipiiie0  42802  sn-0tie0  42815  fourierswlem  46582  3exp4mod41  47970  2t6m3t4e0  48702