Theorem adddii 11360

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242   · cmul 11244

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

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

This theorem is used by:  addrid  11529  3t3e9  12550  numltc  12885  numsucc  12899  numma  12903  decmul10add  12928  4t3lem  12956  9t11e99OLD  12990  decbin2  13002  binom2i  14397  3dec  14451  faclbnd4lem1  14478  3dvds2dec  16547  mod2xnegi  17293  decsplit  17304  log2ublem1  27331  log2ublem2  27332  bposlem8  27675  ax5seglem7  29570  ip0i  31484  ip1ilem  31485  ipasslem10  31498  normlem0  31768  polid2i  31816  lnopunilem1  32669  dfdec100  33517  dpmul10  33557  dpmul  33575  dpmul4  33576  cos9thpiminplylem5  34529  sn-1ne2  43596  sqmid3api  43606  ipiiie0  43755  sn-0tie0  43781  fourierswlem  47513  goldpolyfactor  48200  3exp4mod41  48974  2t6m3t4e0  49791