Theorem adddii 11209

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   · cmul 11093

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

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

This theorem is referenced by:  addrid  11378  3t3e9  12396  numltc  12730  numsucc  12744  numma  12748  decmul10add  12773  4t3lem  12801  9t11e99OLD  12835  decbin2  12847  binom2i  14236  3dec  14290  faclbnd4lem1  14317  3dvds2dec  16379  mod2xnegi  17119  decsplit  17130  log2ublem1  27065  log2ublem2  27066  bposlem8  27409  ax5seglem7  29190  ip0i  31082  ip1ilem  31083  ipasslem10  31096  normlem0  31366  polid2i  31414  lnopunilem1  32267  dfdec100  33082  dpmul10  33122  dpmul  33140  dpmul4  33141  cos9thpiminplylem5  34088  sn-1ne2  42887  sqmid3api  42899  ipiiie0  43054  sn-0tie0  43080  fourierswlem  46803  3exp4mod41  48224  2t6m3t4e0  48980