Theorem adddird 11132

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   + caddc 11004   · cmul 11006

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-addcl 11061  ax-mulcom 11065  ax-distr 11068

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344

This theorem is referenced by:  adddirp1d  11133  joinlmuladdmuld  11134  addmulsub  11574  recextlem1  11742  divdir  11796  subsq  14112  subsq2  14113  binom3  14126  discr1  14141  cshweqrep  14723  remullem  15030  01sqrexlem7  15150  binomlem  15731  binomfallfaclem2  15942  pwp1fsum  16297  smumullem  16398  mul4sqlem  16860  vdwapun  16881  nn0srg  21369  rge0srg  21370  nmotri  24649  blcvx  24708  cphipval2  25163  itg1addlem5  25623  itgconst  25742  dvexp  25879  dvcvx  25947  plyaddlem1  26140  abelthlem7  26370  cxpadd  26610  dcubic  26778  binom4  26782  dquartlem2  26784  dquart  26785  quart1lem  26787  quart1  26788  cvxcl  26917  scvxcvx  26918  basellem9  27021  bposlem9  27225  lgsquad2lem1  27317  2sqlem4  27354  2sqblem  27364  dchrisumlem2  27423  dchrisum0lem1  27449  mudivsum  27463  chpdifbndlem1  27486  pntrlog2bndlem2  27511  pntlemr  27535  pntlemk  27539  ostth2lem2  27567  brbtwn2  28878  ax5seglem3  28904  ax5seglem5  28906  axbtwnid  28912  axeuclidlem  28935  axcontlem2  28938  axcontlem4  28940  axcontlem7  28943  ex-ind-dvds  30433  smcnlem  30669  ccfldsrarelvec  33676  constrrtll  33736  constrrtcclem  33739  constrrtcc  33740  cos9thpiminplylem2  33788  circlemeth  34645  hgt750lemd  34653  logdivsqrle  34655  subfacp1lem6  35221  subfacval2  35223  subfaclim  35224  cvxsconn  35279  resconn  35282  fwddifnp1  36199  itg2addnclem3  37713  itgmulc2nc  37728  rrnequiv  37875  aks4d1p1p7  42107  primrootscoprmpow  42132  3rdpwhole  42325  fltnlta  42696  cu3addd  42714  3cubeslem2  42718  3cubeslem3r  42720  jm2.19lem3  43024  jm2.25  43032  jm3.1lem2  43051  inductionexd  44188  int-leftdistd  44212  binomcxplemwb  44381  binomcxplemnotnn0  44389  sineq0ALT  44969  fperiodmullem  45344  xralrple2  45393  coskpi2  45904  cosknegpi  45907  dvnmul  45981  stoweidlem11  46049  stoweidlem13  46051  stirlinglem1  46112  stirlinglem4  46115  dirkerper  46134  dirkertrigeqlem1  46136  dirkertrigeqlem2  46137  dirkertrigeqlem3  46138  dirkercncflem2  46142  fourierdlem41  46186  fourierdlem42  46187  fourierdlem64  46208  fourierswlem  46268  hoidmvlelem2  46634  sigaraf  46891  fmtnorec3  47579  itscnhlc0yqe  48791  itsclc0yqsollem1  48794  itscnhlc0xyqsol  48797  itsclc0xyqsolr  48801  itsclquadb  48808  2itscplem3  48812  itscnhlinecirc02plem1  48814