Theorem adddii 9929

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  addid1  10095  3t3e9  11057  numltc  11404  numsucc  11425  numma  11433  decmul10add  11469  decmul10addOLD  11470  4t3lem  11507  9t11e99  11547  9t11e99OLD  11548  decbin2  11559  binom2i  12836  3dec  12912  3decOLD  12915  faclbnd4lem1  12942  3dvds2dec  14894  3dvds2decOLD  14895  mod2xnegi  15613  decsplit  15625  decsplitOLD  15629  log2ublem1  24473  log2ublem2  24474  bposlem8  24816  ax5seglem7  25615  ip0i  27064  ip1ilem  27065  ipasslem10  27078  normlem0  27350  polid2i  27398  lnopunilem1  28253  fourierswlem  39123  3exp4mod41  40071  2t6m3t4e0  41919