Theorem adddird 10666

Description: Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddird	⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))

Proof of Theorem adddird

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddir 10632	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-addcl 10597  ax-mulcom 10601  ax-distr 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  adddirp1d  10667  joinlmuladdmuld  10668  addmulsub  11102  recextlem1  11270  divdir  11323  subsq  13573  subsq2  13574  binom3  13586  discr1  13601  cshweqrep  14183  remullem  14487  sqrlem7  14608  binomlem  15184  binomfallfaclem2  15394  pwp1fsum  15742  smumullem  15841  mul4sqlem  16289  vdwapun  16310  nn0srg  20615  rge0srg  20616  nmotri  23348  blcvx  23406  cphipval2  23844  itg1addlem5  24301  itgconst  24419  dvexp  24550  dvcvx  24617  plyaddlem1  24803  abelthlem7  25026  cxpadd  25262  dcubic  25424  binom4  25428  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  cvxcl  25562  scvxcvx  25563  basellem9  25666  bposlem9  25868  lgsquad2lem1  25960  2sqlem4  25997  2sqblem  26007  dchrisumlem2  26066  dchrisum0lem1  26092  mudivsum  26106  chpdifbndlem1  26129  pntrlog2bndlem2  26154  pntlemr  26178  pntlemk  26182  ostth2lem2  26210  brbtwn2  26691  ax5seglem3  26717  ax5seglem5  26719  axbtwnid  26725  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  ex-ind-dvds  28240  smcnlem  28474  ccfldsrarelvec  31056  circlemeth  31911  hgt750lemd  31919  logdivsqrle  31921  subfacp1lem6  32432  subfacval2  32434  subfaclim  32435  cvxsconn  32490  resconn  32493  fwddifnp1  33626  itg2addnclem3  34960  itgmulc2nc  34975  rrnequiv  35128  fltnlta  39295  cu3addd  39297  3cubeslem2  39302  3cubeslem3r  39304  jm2.19lem3  39608  jm2.25  39616  jm3.1lem2  39635  inductionexd  40525  int-leftdistd  40552  binomcxplemwb  40700  binomcxplemnotnn0  40708  sineq0ALT  41291  fperiodmullem  41590  xralrple2  41642  coskpi2  42167  cosknegpi  42170  dvnmul  42248  stoweidlem11  42316  stoweidlem13  42318  stirlinglem1  42379  stirlinglem4  42382  dirkerper  42401  dirkertrigeqlem1  42403  dirkertrigeqlem2  42404  dirkertrigeqlem3  42405  dirkercncflem2  42409  fourierdlem41  42453  fourierdlem42  42454  fourierdlem64  42475  fourierswlem  42535  hoidmvlelem2  42898  sigaraf  43130  fmtnorec3  43730  itscnhlc0yqe  44766  itsclc0yqsollem1  44769  itscnhlc0xyqsol  44772  itsclc0xyqsolr  44776  itsclquadb  44783  2itscplem3  44787  itscnhlinecirc02plem1  44789