Theorem adddii 10988

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

Syntax hints:   = wceq 1542   ∈ wcel 2110  (class class class)co 7271  ℂcc 10870   + caddc 10875   · cmul 10877

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

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

This theorem is referenced by:  addid1  11155  3t3e9  12140  numltc  12462  numsucc  12476  numma  12480  decmul10add  12505  4t3lem  12533  9t11e99  12566  decbin2  12577  binom2i  13926  3dec  13978  faclbnd4lem1  14005  3dvds2dec  16040  mod2xnegi  16770  decsplit  16782  log2ublem1  26094  log2ublem2  26095  bposlem8  26437  ax5seglem7  27301  ip0i  29183  ip1ilem  29184  ipasslem10  29197  normlem0  29467  polid2i  29515  lnopunilem1  30368  dfdec100  31140  dpmul10  31165  dpmul  31183  dpmul4  31184  sn-1ne2  40292  sqmid3api  40308  ipiiie0  40416  sn-0tie0  40418  fourierswlem  43742  3exp4mod41  45037  2t6m3t4e0  45653