Theorem adddii 10389

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

Syntax hints:   = wceq 1601   ∈ wcel 2106  (class class class)co 6922  ℂcc 10270   + caddc 10275   · cmul 10277

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073

This theorem is referenced by:  addid1  10556  3t3e9  11549  numltc  11872  numsucc  11886  numma  11890  decmul10add  11916  4t3lem  11944  9t11e99  11977  decbin2  11988  binom2i  13293  3dec  13371  faclbnd4lem1  13398  3dvds2dec  15461  mod2xnegi  16179  decsplit  16191  log2ublem1  25125  log2ublem2  25126  bposlem8  25468  ax5seglem7  26284  ip0i  28266  ip1ilem  28267  ipasslem10  28280  normlem0  28552  polid2i  28600  lnopunilem1  29455  dfdec100  30154  dpmul10  30179  dpmul  30197  dpmul4  30198  sqmid3api  38141  fourierswlem  41366  3exp4mod41  42546  2t6m3t4e0  43133