Theorem adddii 11222

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104   · cmul 11106

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  addrid  11391  3t3e9  12409  numltc  12743  numsucc  12757  numma  12761  decmul10add  12786  4t3lem  12814  9t11e99OLD  12848  decbin2  12860  binom2i  14250  3dec  14304  faclbnd4lem1  14331  3dvds2dec  16392  mod2xnegi  17132  decsplit  17143  log2ublem1  27092  log2ublem2  27093  bposlem8  27436  ax5seglem7  29266  ip0i  31158  ip1ilem  31159  ipasslem10  31172  normlem0  31442  polid2i  31490  lnopunilem1  32343  dfdec100  33155  dpmul10  33195  dpmul  33213  dpmul4  33214  cos9thpiminplylem5  34157  sn-1ne2  43013  sqmid3api  43025  ipiiie0  43180  sn-0tie0  43206  fourierswlem  46927  3exp4mod41  48351  2t6m3t4e0  49111