Theorem adddii 11232

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  (class class class)co 7413  ℂcc 11112   + caddc 11117   · cmul 11119

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087

This theorem is referenced by:  addrid  11400  3t3e9  12385  numltc  12709  numsucc  12723  numma  12727  decmul10add  12752  4t3lem  12780  9t11e99  12813  decbin2  12824  binom2i  14182  3dec  14232  faclbnd4lem1  14259  3dvds2dec  16282  mod2xnegi  17010  decsplit  17022  log2ublem1  26685  log2ublem2  26686  bposlem8  27028  ax5seglem7  28458  ip0i  30343  ip1ilem  30344  ipasslem10  30357  normlem0  30627  polid2i  30675  lnopunilem1  31528  dfdec100  32301  dpmul10  32326  dpmul  32344  dpmul4  32345  sn-1ne2  41483  sqmid3api  41499  ipiiie0  41614  sn-0tie0  41616  fourierswlem  45246  3exp4mod41  46584  2t6m3t4e0  47114