Theorem adddii 10987

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874   · cmul 10876

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  addid1  11155  3t3e9  12140  numltc  12463  numsucc  12477  numma  12481  decmul10add  12506  4t3lem  12534  9t11e99  12567  decbin2  12578  binom2i  13928  3dec  13980  faclbnd4lem1  14007  3dvds2dec  16042  mod2xnegi  16772  decsplit  16784  log2ublem1  26096  log2ublem2  26097  bposlem8  26439  ax5seglem7  27303  ip0i  29187  ip1ilem  29188  ipasslem10  29201  normlem0  29471  polid2i  29519  lnopunilem1  30372  dfdec100  31144  dpmul10  31169  dpmul  31187  dpmul4  31188  sn-1ne2  40295  sqmid3api  40311  ipiiie0  40419  sn-0tie0  40421  fourierswlem  43771  3exp4mod41  45068  2t6m3t4e0  45684