Theorem adddii 11270

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155   · cmul 11157

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

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

This theorem is referenced by:  addrid  11438  3t3e9  12430  numltc  12756  numsucc  12770  numma  12774  decmul10add  12799  4t3lem  12827  9t11e99  12860  decbin2  12871  binom2i  14247  3dec  14301  faclbnd4lem1  14328  3dvds2dec  16366  mod2xnegi  17104  decsplit  17116  log2ublem1  27003  log2ublem2  27004  bposlem8  27349  ax5seglem7  28964  ip0i  30853  ip1ilem  30854  ipasslem10  30867  normlem0  31137  polid2i  31185  lnopunilem1  32038  dfdec100  32836  dpmul10  32861  dpmul  32879  dpmul4  32880  sn-1ne2  42278  sqmid3api  42296  ipiiie0  42443  sn-0tie0  42445  fourierswlem  46185  3exp4mod41  47540  2t6m3t4e0  48192