Theorem adddii 11245

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   + caddc 11127   · cmul 11129

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

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

This theorem is used by:  addrid  11414  3t3e9  12432  numltc  12767  numsucc  12781  numma  12785  decmul10add  12810  4t3lem  12838  9t11e99OLD  12872  decbin2  12884  binom2i  14276  3dec  14330  faclbnd4lem1  14357  3dvds2dec  16423  mod2xnegi  17163  decsplit  17174  log2ublem1  27183  log2ublem2  27184  bposlem8  27527  ax5seglem7  29392  ip0i  31306  ip1ilem  31307  ipasslem10  31320  normlem0  31590  polid2i  31638  lnopunilem1  32491  dfdec100  33300  dpmul10  33340  dpmul  33358  dpmul4  33359  cos9thpiminplylem5  34296  sn-1ne2  43146  sqmid3api  43158  ipiiie0  43313  sn-0tie0  43339  fourierswlem  47058  goldpolyfactor  47745  3exp4mod41  48519  2t6m3t4e0  49278