Theorem adddii 11144

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031

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

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

This theorem is referenced by:  addrid  11313  3t3e9  12307  numltc  12633  numsucc  12647  numma  12651  decmul10add  12676  4t3lem  12704  9t11e99  12737  decbin2  12748  binom2i  14135  3dec  14189  faclbnd4lem1  14216  3dvds2dec  16260  mod2xnegi  16999  decsplit  17010  log2ublem1  26912  log2ublem2  26913  bposlem8  27258  ax5seglem7  29008  ip0i  30900  ip1ilem  30901  ipasslem10  30914  normlem0  31184  polid2i  31232  lnopunilem1  32085  dfdec100  32911  dpmul10  32976  dpmul  32994  dpmul4  32995  cos9thpiminplylem5  33943  sn-1ne2  42516  sqmid3api  42534  ipiiie0  42689  sn-0tie0  42702  fourierswlem  46470  3exp4mod41  47858  2t6m3t4e0  48590