Theorem adddii 11124

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009   · cmul 11011

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

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

This theorem is referenced by:  addrid  11293  3t3e9  12287  numltc  12614  numsucc  12628  numma  12632  decmul10add  12657  4t3lem  12685  9t11e99  12718  decbin2  12729  binom2i  14119  3dec  14173  faclbnd4lem1  14200  3dvds2dec  16244  mod2xnegi  16983  decsplit  16994  log2ublem1  26884  log2ublem2  26885  bposlem8  27230  ax5seglem7  28914  ip0i  30803  ip1ilem  30804  ipasslem10  30817  normlem0  31087  polid2i  31135  lnopunilem1  31988  dfdec100  32811  dpmul10  32873  dpmul  32891  dpmul4  32892  cos9thpiminplylem5  33797  sn-1ne2  42304  sqmid3api  42322  ipiiie0  42477  sn-0tie0  42490  fourierswlem  46274  3exp4mod41  47653  2t6m3t4e0  48385