Theorem adddii 11256

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136   + caddc 11141   · cmul 11143

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  addrid  11424  3t3e9  12409  numltc  12733  numsucc  12747  numma  12751  decmul10add  12776  4t3lem  12804  9t11e99  12837  decbin2  12848  binom2i  14207  3dec  14257  faclbnd4lem1  14284  3dvds2dec  16309  mod2xnegi  17039  decsplit  17051  log2ublem1  26877  log2ublem2  26878  bposlem8  27223  ax5seglem7  28745  ip0i  30634  ip1ilem  30635  ipasslem10  30648  normlem0  30918  polid2i  30966  lnopunilem1  31819  dfdec100  32593  dpmul10  32618  dpmul  32636  dpmul4  32637  sn-1ne2  41840  sqmid3api  41857  ipiiie0  41992  sn-0tie0  41994  fourierswlem  45618  3exp4mod41  46956  2t6m3t4e0  47412