Theorem adddird 11239

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-addcl 11170  ax-mulcom 11174  ax-distr 11177

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  adddirp1d  11240  joinlmuladdmuld  11241  addmulsub  11676  recextlem1  11844  divdir  11897  subsq  14174  subsq2  14175  binom3  14187  discr1  14202  cshweqrep  14771  remullem  15075  01sqrexlem7  15195  binomlem  15775  binomfallfaclem2  15984  pwp1fsum  16334  smumullem  16433  mul4sqlem  16886  vdwapun  16907  nn0srg  21015  rge0srg  21016  nmotri  24256  blcvx  24314  cphipval2  24758  itg1addlem5  25218  itgconst  25336  dvexp  25470  dvcvx  25537  plyaddlem1  25727  abelthlem7  25950  cxpadd  26187  dcubic  26351  binom4  26355  dquartlem2  26357  dquart  26358  quart1lem  26360  quart1  26361  cvxcl  26489  scvxcvx  26490  basellem9  26593  bposlem9  26795  lgsquad2lem1  26887  2sqlem4  26924  2sqblem  26934  dchrisumlem2  26993  dchrisum0lem1  27019  mudivsum  27033  chpdifbndlem1  27056  pntrlog2bndlem2  27081  pntlemr  27105  pntlemk  27109  ostth2lem2  27137  brbtwn2  28163  ax5seglem3  28189  ax5seglem5  28191  axbtwnid  28197  axeuclidlem  28220  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  ex-ind-dvds  29714  smcnlem  29950  ccfldsrarelvec  32745  circlemeth  33652  hgt750lemd  33660  logdivsqrle  33662  subfacp1lem6  34176  subfacval2  34178  subfaclim  34179  cvxsconn  34234  resconn  34237  fwddifnp1  35137  itg2addnclem3  36541  itgmulc2nc  36556  rrnequiv  36703  aks4d1p1p7  40939  fltnlta  41405  cu3addd  41418  3cubeslem2  41423  3cubeslem3r  41425  jm2.19lem3  41730  jm2.25  41738  jm3.1lem2  41757  inductionexd  42906  int-leftdistd  42931  binomcxplemwb  43107  binomcxplemnotnn0  43115  sineq0ALT  43698  fperiodmullem  44013  xralrple2  44064  coskpi2  44582  cosknegpi  44585  dvnmul  44659  stoweidlem11  44727  stoweidlem13  44729  stirlinglem1  44790  stirlinglem4  44793  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkercncflem2  44820  fourierdlem41  44864  fourierdlem42  44865  fourierdlem64  44886  fourierswlem  44946  hoidmvlelem2  45312  sigaraf  45569  fmtnorec3  46216  itscnhlc0yqe  47445  itsclc0yqsollem1  47448  itscnhlc0xyqsol  47451  itsclc0xyqsolr  47455  itsclquadb  47462  2itscplem3  47466  itscnhlinecirc02plem1  47468