Theorem adddiri 11223

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-addcl 11161  ax-mulcom 11165  ax-distr 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  numma  12761  binom2i  14250  3dvdsdec  16391  3dvds2dec  16392  dec5nprm  17127  dec2nprm  17128  mod2xnegi  17132  karatsuba  17144  sincosq3sgn  26643  sincosq4sgn  26644  ang180lem2  26953  1cubrlem  26984  bposlem8  27433  2lgsoddprmlem3c  27554  2lgsoddprmlem3d  27555  normlem3  31442  dpmul100  33194  dpmul1000  33196  dpadd3  33209  dpmul4  33211  cos9thpiminplylem5  34154  problem2  36136  areaquad  43923  tgoldbachlt  48558