Theorem adddii 11325

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7421  ℂcc 11202   + caddc 11207   · cmul 11209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11271

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11494  3t3e9  12514  numltc  12849  numsucc  12863  numma  12867  decmul10add  12892  4t3lem  12920  9t11e99OLD  12954  decbin2  12966  binom2i  14360  3dec  14414  faclbnd4lem1  14441  3dvds2dec  16509  mod2xnegi  17255  decsplit  17266  log2ublem1  27280  log2ublem2  27281  bposlem8  27624  ax5seglem7  29519  ip0i  31433  ip1ilem  31434  ipasslem10  31447  normlem0  31717  polid2i  31765  lnopunilem1  32618  dfdec100  33468  dpmul10  33508  dpmul  33526  dpmul4  33527  cos9thpiminplylem5  34465  sn-1ne2  43424  sqmid3api  43434  ipiiie0  43583  sn-0tie0  43609  fourierswlem  47334  goldpolyfactor  48021  3exp4mod41  48795  2t6m3t4e0  49554