Theorem adddii 11193

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   · cmul 11080

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11361  3t3e9  12355  numltc  12682  numsucc  12696  numma  12700  decmul10add  12725  4t3lem  12753  9t11e99  12786  decbin2  12797  binom2i  14184  3dec  14238  faclbnd4lem1  14265  3dvds2dec  16310  mod2xnegi  17049  decsplit  17060  log2ublem1  26863  log2ublem2  26864  bposlem8  27209  ax5seglem7  28869  ip0i  30761  ip1ilem  30762  ipasslem10  30775  normlem0  31045  polid2i  31093  lnopunilem1  31946  dfdec100  32762  dpmul10  32822  dpmul  32840  dpmul4  32841  cos9thpiminplylem5  33783  sn-1ne2  42260  sqmid3api  42278  ipiiie0  42433  sn-0tie0  42446  fourierswlem  46235  3exp4mod41  47621  2t6m3t4e0  48340