Theorem adddird 11229

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098   · cmul 11100

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 11155  ax-mulcom 11159  ax-distr 11162

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 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  adddirp1d  11230  joinlmuladdmuld  11231  addmulsub  11671  recextlem1  11839  divdir  11892  subsq  14242  subsq2  14243  binom3  14256  discr1  14271  cshweqrep  14854  remullem  15175  01sqrexlem7  15295  binomlem  15879  binomfallfaclem2  16089  pwp1fsum  16444  smumullem  16545  mul4sqlem  17008  vdwapun  17029  nn0srg  21587  rge0srg  21588  nmotri  24896  blcvx  24955  cphipval2  25400  itg1addlem5  25859  itgconst  25978  dvexp  26112  dvcvx  26179  plyaddlem1  26370  abelthlem7  26601  cxpadd  26844  dcubic  27011  binom4  27015  dquartlem2  27017  dquart  27018  quart1lem  27020  quart1  27021  cvxcl  27149  scvxcvx  27150  basellem9  27253  bposlem9  27456  lgsquad2lem1  27548  2sqlem4  27585  2sqblem  27595  dchrisumlem2  27654  dchrisum0lem1  27680  mudivsum  27694  chpdifbndlem1  27717  pntrlog2bndlem2  27742  pntlemr  27766  pntlemk  27770  ostth2lem2  27798  brbtwn2  29255  ax5seglem3  29281  ax5seglem5  29283  axbtwnid  29289  axeuclidlem  29312  axcontlem2  29315  axcontlem4  29317  axcontlem7  29320  ex-ind-dvds  30812  smcnlem  31049  ccfldsrarelvec  34061  constrrtll  34121  constrrtcclem  34124  constrrtcc  34125  cos9thpiminplylem2  34173  circlemeth  35027  hgt750lemd  35035  logdivsqrle  35037  subfacp1lem6  35677  subfacval2  35679  subfaclim  35680  cvxsconn  35735  resconn  35738  fwddifnp1  36657  itg2addnclem3  38324  itgmulc2nc  38339  rrnequiv  38486  aks4d1p1p7  42841  primrootscoprmpow  42866  3rdpwhole  43053  fltnlta  43395  cu3addd  43412  3cubeslem2  43416  3cubeslem3r  43418  jm2.19lem3  43718  jm2.25  43726  jm3.1lem2  43745  inductionexd  44881  int-leftdistd  44905  binomcxplemwb  45058  binomcxplemnotnn0  45066  sineq0ALT  45645  fperiodmullem  46022  xralrple2  46070  coskpi2  46580  cosknegpi  46583  dvnmul  46657  stoweidlem11  46725  stoweidlem13  46727  stirlinglem1  46788  stirlinglem4  46791  dirkerper  46810  dirkertrigeqlem1  46812  dirkertrigeqlem2  46813  dirkertrigeqlem3  46814  dirkercncflem2  46818  fourierdlem41  46862  fourierdlem42  46863  fourierdlem64  46884  fourierswlem  46944  hoidmvlelem2  47310  sigaraf  47567  sin3t  47608  cos3t  47609  sin5tlem1  47610  sin5tlem5  47614  sin5t  47615  cos5t  47616  fmtnorec3  48300  itscnhlc0yqe  49539  itsclc0yqsollem1  49542  itscnhlc0xyqsol  49545  itsclc0xyqsolr  49549  itsclquadb  49556  2itscplem3  49560  itscnhlinecirc02plem1  49562