Theorem adddii 11232

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7416  ℂcc 11109   + caddc 11114   · cmul 11116

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11401  3t3e9  12419  numltc  12753  numsucc  12767  numma  12771  decmul10add  12796  4t3lem  12824  9t11e99OLD  12858  decbin2  12870  binom2i  14261  3dec  14315  faclbnd4lem1  14342  3dvds2dec  16408  mod2xnegi  17148  decsplit  17159  log2ublem1  27140  log2ublem2  27141  bposlem8  27484  ax5seglem7  29314  ip0i  31206  ip1ilem  31207  ipasslem10  31220  normlem0  31490  polid2i  31538  lnopunilem1  32391  dfdec100  33203  dpmul10  33243  dpmul  33261  dpmul4  33262  cos9thpiminplylem5  34199  sn-1ne2  43065  sqmid3api  43077  ipiiie0  43232  sn-0tie0  43258  fourierswlem  46977  3exp4mod41  48401  2t6m3t4e0  49161