Theorem adddii 11209

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  addrid  11378  3t3e9  12399  numltc  12733  numsucc  12747  numma  12751  decmul10add  12776  4t3lem  12804  9t11e99OLD  12838  decbin2  12850  binom2i  14239  3dec  14293  faclbnd4lem1  14320  3dvds2dec  16381  mod2xnegi  17121  decsplit  17132  log2ublem1  27069  log2ublem2  27070  bposlem8  27413  ax5seglem7  29194  ip0i  31086  ip1ilem  31087  ipasslem10  31100  normlem0  31370  polid2i  31418  lnopunilem1  32271  dfdec100  33087  dpmul10  33127  dpmul  33145  dpmul4  33146  cos9thpiminplylem5  34093  sn-1ne2  42892  sqmid3api  42904  ipiiie0  43059  sn-0tie0  43085  fourierswlem  46802  3exp4mod41  48223  2t6m3t4e0  48979