Theorem adddiri 11325

Description: Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
adddiri	⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))

Proof of Theorem adddiri

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		adddir 11300	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1490	1 ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   + caddc 11206   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-addcl 11263  ax-mulcom 11267  ax-distr 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  numma  12866  binom2i  14359  3dvdsdec  16507  3dvds2dec  16508  dec5nprm  17249  dec2nprm  17250  mod2xnegi  17254  karatsuba  17266  sincosq3sgn  26834  sincosq4sgn  26835  ang180lem2  27143  1cubrlem  27174  bposlem8  27623  2lgsoddprmlem3c  27744  2lgsoddprmlem3d  27745  normlem3  31719  dpmul100  33509  dpmul1000  33511  dpadd3  33524  dpmul4  33526  cos9thpiminplylem5  34464  problem2  36517  areaquad  44311  goldpolyfactor  48020  goldratmolem3  48027  tgoldbachlt  49007