Theorem adddird 11339

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7422  ℂcc 11203   + caddc 11208   · cmul 11210

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-addcl 11265  ax-mulcom 11269  ax-distr 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549  df-ov 7425

This theorem is used by:  adddirp1d  11340  joinlmuladdmuld  11341  addmulsub  11783  recextlem1  11951  divdir  12004  subsq  14359  subsq2  14360  binom3  14373  discr1  14388  cshweqrep  14978  remullem  15302  01sqrexlem7  15422  binomlem  16005  binomfallfaclem2  16213  pwp1fsum  16568  smumullem  16669  mul4sqlem  17138  vdwapun  17159  nn0srg  21750  rge0srg  21751  nmotri  25065  blcvx  25124  cphipval2  25569  itg1addlem5  26028  itgconst  26146  dvexp  26280  dvcvx  26347  plyaddlem1  26539  abelthlem7  26772  cxpadd  27014  dcubic  27181  binom4  27185  dquartlem2  27187  dquart  27188  quart1lem  27190  quart1  27191  cvxcl  27319  scvxcvx  27320  basellem9  27423  bposlem9  27626  lgsquad2lem1  27718  2sqlem4  27755  2sqblem  27765  dchrisumlem2  27824  dchrisum0lem1  27850  mudivsum  27864  chpdifbndlem1  27887  pntrlog2bndlem2  27912  pntlemr  27936  pntlemk  27940  ostth2lem2  27968  brbtwn2  29490  ax5seglem3  29516  ax5seglem5  29518  axbtwnid  29524  axeuclidlem  29547  axcontlem2  29550  axcontlem4  29552  axcontlem7  29555  ex-ind-dvds  31069  smcnlem  31306  ccfldsrarelvec  34351  constrrtll  34411  constrrtcclem  34414  constrrtcc  34415  cos9thpiminplylem2  34463  circlemeth  35317  hgt750lemd  35325  logdivsqrle  35327  subfacp1lem6  36038  subfacval2  36040  subfaclim  36041  cvxsconn  36096  resconn  36099  fwddifnp1  37024  itg2addnclem3  38698  itgmulc2nc  38713  rrnequiv  38876  aks4d1p1p7  43231  primrootscoprmpow  43256  3rdpwhole  43456  fltnlta  43781  cu3addd  43798  3cubeslem2  43802  3cubeslem3r  43804  jm2.19lem3  44105  jm2.25  44113  jm3.1lem2  44132  inductionexd  45262  int-leftdistd  45286  binomcxplemwb  45439  binomcxplemnotnn0  45447  sineq0ALT  46026  fperiodmullem  46426  xralrple2  46473  coskpi2  46983  cosknegpi  46986  dvnmul  47060  stoweidlem11  47128  stoweidlem13  47130  stirlinglem1  47191  stirlinglem4  47194  dirkerper  47213  dirkertrigeqlem1  47215  dirkertrigeqlem2  47216  dirkertrigeqlem3  47217  dirkercncflem2  47221  fourierdlem41  47265  fourierdlem42  47266  fourierdlem64  47287  fourierswlem  47347  hoidmvlelem2  47713  sigaraf  47970  sin3t  48024  cos3t  48025  sin5tlem1  48026  sin5tlem5  48030  sin5t  48031  cos5t  48032  fmtnorec3  48740  itscnhlc0yqe  49978  itsclc0yqsollem1  49981  itscnhlc0xyqsol  49984  itsclc0xyqsolr  49988  itsclquadb  49995  2itscplem3  49999  itscnhlinecirc02plem1  50001  crossp3d  51149