Theorem adddii 11148

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032   · cmul 11034

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

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

This theorem is referenced by:  addrid  11317  3t3e9  12334  numltc  12661  numsucc  12675  numma  12679  decmul10add  12704  4t3lem  12732  9t11e99  12765  decbin2  12776  binom2i  14165  3dec  14219  faclbnd4lem1  14246  3dvds2dec  16293  mod2xnegi  17033  decsplit  17044  log2ublem1  26923  log2ublem2  26924  bposlem8  27268  ax5seglem7  29018  ip0i  30911  ip1ilem  30912  ipasslem10  30925  normlem0  31195  polid2i  31243  lnopunilem1  32096  dfdec100  32918  dpmul10  32969  dpmul  32987  dpmul4  32988  cos9thpiminplylem5  33946  sn-1ne2  42717  sqmid3api  42729  ipiiie0  42884  sn-0tie0  42910  fourierswlem  46676  3exp4mod41  48091  2t6m3t4e0  48836