Theorem adddird 11161

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032   · cmul 11034

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 11089  ax-mulcom 11093  ax-distr 11096

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  adddirp1d  11162  joinlmuladdmuld  11163  addmulsub  11603  recextlem1  11771  divdir  11825  subsq  14163  subsq2  14164  binom3  14177  discr1  14192  cshweqrep  14774  remullem  15081  01sqrexlem7  15201  binomlem  15785  binomfallfaclem2  15996  pwp1fsum  16351  smumullem  16452  mul4sqlem  16915  vdwapun  16936  nn0srg  21427  rge0srg  21428  nmotri  24714  blcvx  24773  cphipval2  25218  itg1addlem5  25677  itgconst  25796  dvexp  25930  dvcvx  25997  plyaddlem1  26188  abelthlem7  26416  cxpadd  26656  dcubic  26823  binom4  26827  dquartlem2  26829  dquart  26830  quart1lem  26832  quart1  26833  cvxcl  26962  scvxcvx  26963  basellem9  27066  bposlem9  27269  lgsquad2lem1  27361  2sqlem4  27398  2sqblem  27408  dchrisumlem2  27467  dchrisum0lem1  27493  mudivsum  27507  chpdifbndlem1  27530  pntrlog2bndlem2  27555  pntlemr  27579  pntlemk  27583  ostth2lem2  27611  brbtwn2  28988  ax5seglem3  29014  ax5seglem5  29016  axbtwnid  29022  axeuclidlem  29045  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  ex-ind-dvds  30546  smcnlem  30783  ccfldsrarelvec  33831  constrrtll  33891  constrrtcclem  33894  constrrtcc  33895  cos9thpiminplylem2  33943  circlemeth  34800  hgt750lemd  34808  logdivsqrle  34810  subfacp1lem6  35383  subfacval2  35385  subfaclim  35386  cvxsconn  35441  resconn  35444  fwddifnp1  36363  itg2addnclem3  38008  itgmulc2nc  38023  rrnequiv  38170  aks4d1p1p7  42527  primrootscoprmpow  42552  3rdpwhole  42738  fltnlta  43110  cu3addd  43127  3cubeslem2  43131  3cubeslem3r  43133  jm2.19lem3  43437  jm2.25  43445  jm3.1lem2  43464  inductionexd  44600  int-leftdistd  44624  binomcxplemwb  44793  binomcxplemnotnn0  44801  sineq0ALT  45381  fperiodmullem  45754  xralrple2  45802  coskpi2  46312  cosknegpi  46315  dvnmul  46389  stoweidlem11  46457  stoweidlem13  46459  stirlinglem1  46520  stirlinglem4  46523  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkercncflem2  46550  fourierdlem41  46594  fourierdlem42  46595  fourierdlem64  46616  fourierswlem  46676  hoidmvlelem2  47042  sigaraf  47299  sin3t  47335  cos3t  47336  sin5tlem1  47337  sin5tlem5  47341  sin5t  47342  fmtnorec3  48023  itscnhlc0yqe  49247  itsclc0yqsollem1  49250  itscnhlc0xyqsol  49253  itsclc0xyqsolr  49257  itsclquadb  49264  2itscplem3  49268  itscnhlinecirc02plem1  49270