Theorem adddii 11191

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   + caddc 11073   · cmul 11075

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  addrid  11360  3t3e9  12382  numltc  12716  numsucc  12730  numma  12734  decmul10add  12759  4t3lem  12787  9t11e99OLD  12821  decbin2  12833  binom2i  14222  3dec  14276  faclbnd4lem1  14303  3dvds2dec  16350  mod2xnegi  17090  decsplit  17101  log2ublem1  26988  log2ublem2  26989  bposlem8  27332  ax5seglem7  29082  ip0i  30974  ip1ilem  30975  ipasslem10  30988  normlem0  31258  polid2i  31306  lnopunilem1  32159  dfdec100  32982  dpmul10  33033  dpmul  33051  dpmul4  33052  cos9thpiminplylem5  34044  sn-1ne2  42844  sqmid3api  42856  ipiiie0  43011  sn-0tie0  43037  fourierswlem  46768  3exp4mod41  48189  2t6m3t4e0  48934