Theorem adddii 10647

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

Syntax hints:   = wceq 1533   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529   + caddc 10534   · cmul 10536

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  addid1  10814  3t3e9  11798  numltc  12118  numsucc  12132  numma  12136  decmul10add  12161  4t3lem  12189  9t11e99  12222  decbin2  12233  binom2i  13568  3dec  13620  faclbnd4lem1  13647  3dvds2dec  15676  mod2xnegi  16401  decsplit  16413  log2ublem1  25518  log2ublem2  25519  bposlem8  25861  ax5seglem7  26715  ip0i  28596  ip1ilem  28597  ipasslem10  28610  normlem0  28880  polid2i  28928  lnopunilem1  29781  dfdec100  30541  dpmul10  30566  dpmul  30584  dpmul4  30585  sn-1ne2  39151  sqmid3api  39162  fourierswlem  42508  3exp4mod41  43774  2t6m3t4e0  44389