Theorem adddii 11302

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   · cmul 11189

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  addrid  11470  3t3e9  12460  numltc  12784  numsucc  12798  numma  12802  decmul10add  12827  4t3lem  12855  9t11e99  12888  decbin2  12899  binom2i  14261  3dec  14315  faclbnd4lem1  14342  3dvds2dec  16381  mod2xnegi  17118  decsplit  17130  log2ublem1  27007  log2ublem2  27008  bposlem8  27353  ax5seglem7  28968  ip0i  30857  ip1ilem  30858  ipasslem10  30871  normlem0  31141  polid2i  31189  lnopunilem1  32042  dfdec100  32834  dpmul10  32859  dpmul  32877  dpmul4  32878  sn-1ne2  42254  sqmid3api  42272  ipiiie0  42413  sn-0tie0  42415  fourierswlem  46151  3exp4mod41  47490  2t6m3t4e0  48073