Theorem adddii 11157

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 7367  ℂ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  11326  3t3e9  12343  numltc  12670  numsucc  12684  numma  12688  decmul10add  12713  4t3lem  12741  9t11e99  12774  decbin2  12785  binom2i  14174  3dec  14228  faclbnd4lem1  14255  3dvds2dec  16302  mod2xnegi  17042  decsplit  17053  log2ublem1  26910  log2ublem2  26911  bposlem8  27254  ax5seglem7  29004  ip0i  30896  ip1ilem  30897  ipasslem10  30910  normlem0  31180  polid2i  31228  lnopunilem1  32081  dfdec100  32903  dpmul10  32954  dpmul  32972  dpmul4  32973  cos9thpiminplylem5  33930  sn-1ne2  42703  sqmid3api  42715  ipiiie0  42870  sn-0tie0  42896  fourierswlem  46658  3exp4mod41  48079  2t6m3t4e0  48824