Theorem adddird 11169

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-addcl 11098  ax-mulcom 11102  ax-distr 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  adddirp1d  11170  joinlmuladdmuld  11171  addmulsub  11611  recextlem1  11779  divdir  11833  subsq  14145  subsq2  14146  binom3  14159  discr1  14174  cshweqrep  14756  remullem  15063  01sqrexlem7  15183  binomlem  15764  binomfallfaclem2  15975  pwp1fsum  16330  smumullem  16431  mul4sqlem  16893  vdwapun  16914  nn0srg  21404  rge0srg  21405  nmotri  24695  blcvx  24754  cphipval2  25209  itg1addlem5  25669  itgconst  25788  dvexp  25925  dvcvx  25993  plyaddlem1  26186  abelthlem7  26416  cxpadd  26656  dcubic  26824  binom4  26828  dquartlem2  26830  dquart  26831  quart1lem  26833  quart1  26834  cvxcl  26963  scvxcvx  26964  basellem9  27067  bposlem9  27271  lgsquad2lem1  27363  2sqlem4  27400  2sqblem  27410  dchrisumlem2  27469  dchrisum0lem1  27495  mudivsum  27509  chpdifbndlem1  27532  pntrlog2bndlem2  27557  pntlemr  27581  pntlemk  27585  ostth2lem2  27613  brbtwn2  28990  ax5seglem3  29016  ax5seglem5  29018  axbtwnid  29024  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  ex-ind-dvds  30548  smcnlem  30785  ccfldsrarelvec  33849  constrrtll  33909  constrrtcclem  33912  constrrtcc  33913  cos9thpiminplylem2  33961  circlemeth  34818  hgt750lemd  34826  logdivsqrle  34828  subfacp1lem6  35401  subfacval2  35403  subfaclim  35404  cvxsconn  35459  resconn  35462  fwddifnp1  36381  itg2addnclem3  37924  itgmulc2nc  37939  rrnequiv  38086  aks4d1p1p7  42444  primrootscoprmpow  42469  3rdpwhole  42662  fltnlta  43021  cu3addd  43038  3cubeslem2  43042  3cubeslem3r  43044  jm2.19lem3  43348  jm2.25  43356  jm3.1lem2  43375  inductionexd  44511  int-leftdistd  44535  binomcxplemwb  44704  binomcxplemnotnn0  44712  sineq0ALT  45292  fperiodmullem  45665  xralrple2  45713  coskpi2  46224  cosknegpi  46227  dvnmul  46301  stoweidlem11  46369  stoweidlem13  46371  stirlinglem1  46432  stirlinglem4  46435  dirkerper  46454  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkercncflem2  46462  fourierdlem41  46506  fourierdlem42  46507  fourierdlem64  46528  fourierswlem  46588  hoidmvlelem2  46954  sigaraf  47211  fmtnorec3  47908  itscnhlc0yqe  49119  itsclc0yqsollem1  49122  itscnhlc0xyqsol  49125  itsclc0xyqsolr  49129  itsclquadb  49136  2itscplem3  49140  itscnhlinecirc02plem1  49142