Theorem adddii 11145

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   + caddc 11030   · cmul 11032

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

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

This theorem is referenced by:  addrid  11314  3t3e9  12308  numltc  12634  numsucc  12648  numma  12652  decmul10add  12677  4t3lem  12705  9t11e99  12738  decbin2  12749  binom2i  14136  3dec  14190  faclbnd4lem1  14217  3dvds2dec  16261  mod2xnegi  17000  decsplit  17011  log2ublem1  26896  log2ublem2  26897  bposlem8  27242  ax5seglem7  28992  ip0i  30885  ip1ilem  30886  ipasslem10  30899  normlem0  31169  polid2i  31217  lnopunilem1  32070  dfdec100  32894  dpmul10  32959  dpmul  32977  dpmul4  32978  cos9thpiminplylem5  33936  sn-1ne2  42696  sqmid3api  42714  ipiiie0  42869  sn-0tie0  42895  fourierswlem  46662  3exp4mod41  48050  2t6m3t4e0  48782