Theorem adddii 11155

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039   · cmul 11041

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  addrid  11324  3t3e9  12341  numltc  12668  numsucc  12682  numma  12686  decmul10add  12711  4t3lem  12739  9t11e99  12772  decbin2  12783  binom2i  14172  3dec  14226  faclbnd4lem1  14253  3dvds2dec  16300  mod2xnegi  17040  decsplit  17051  log2ublem1  26935  log2ublem2  26936  bposlem8  27279  ax5seglem7  29029  ip0i  30921  ip1ilem  30922  ipasslem10  30935  normlem0  31205  polid2i  31253  lnopunilem1  32106  dfdec100  32929  dpmul10  32980  dpmul  32998  dpmul4  32999  cos9thpiminplylem5  33977  sn-1ne2  42755  sqmid3api  42767  ipiiie0  42922  sn-0tie0  42948  fourierswlem  46680  3exp4mod41  48101  2t6m3t4e0  48846