Theorem adddii 11314

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191   + caddc 11196   · cmul 11198

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

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

This theorem is used by:  addrid  11483  3t3e9  12503  numltc  12838  numsucc  12852  numma  12856  decmul10add  12881  4t3lem  12909  9t11e99OLD  12943  decbin2  12955  binom2i  14349  3dec  14403  faclbnd4lem1  14430  3dvds2dec  16496  mod2xnegi  17242  decsplit  17253  log2ublem1  27267  log2ublem2  27268  bposlem8  27611  ax5seglem7  29506  ip0i  31420  ip1ilem  31421  ipasslem10  31434  normlem0  31704  polid2i  31752  lnopunilem1  32605  dfdec100  33414  dpmul10  33454  dpmul  33472  dpmul4  33473  cos9thpiminplylem5  34411  sn-1ne2  43310  sqmid3api  43320  ipiiie0  43469  sn-0tie0  43495  fourierswlem  47209  goldpolyfactor  47896  3exp4mod41  48670  2t6m3t4e0  49429