Theorem adddird 11258

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   + caddc 11127   · cmul 11129

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-addcl 11184  ax-mulcom 11188  ax-distr 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416

This theorem is used by:  adddirp1d  11259  joinlmuladdmuld  11260  addmulsub  11700  recextlem1  11868  divdir  11921  subsq  14274  subsq2  14275  binom3  14288  discr1  14303  cshweqrep  14892  remullem  15215  01sqrexlem7  15335  binomlem  15918  binomfallfaclem2  16126  pwp1fsum  16481  smumullem  16582  mul4sqlem  17045  vdwapun  17066  nn0srg  21650  rge0srg  21651  nmotri  24965  blcvx  25024  cphipval2  25469  itg1addlem5  25928  itgconst  26046  dvexp  26180  dvcvx  26247  plyaddlem1  26439  abelthlem7  26674  cxpadd  26916  dcubic  27083  binom4  27087  dquartlem2  27089  dquart  27090  quart1lem  27092  quart1  27093  cvxcl  27221  scvxcvx  27222  basellem9  27325  bposlem9  27528  lgsquad2lem1  27620  2sqlem4  27657  2sqblem  27667  dchrisumlem2  27726  dchrisum0lem1  27752  mudivsum  27766  chpdifbndlem1  27789  pntrlog2bndlem2  27814  pntlemr  27838  pntlemk  27842  ostth2lem2  27870  brbtwn2  29362  ax5seglem3  29388  ax5seglem5  29390  axbtwnid  29396  axeuclidlem  29419  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  ex-ind-dvds  30941  smcnlem  31178  ccfldsrarelvec  34181  constrrtll  34241  constrrtcclem  34244  constrrtcc  34245  cos9thpiminplylem2  34293  circlemeth  35148  hgt750lemd  35156  logdivsqrle  35158  subfacp1lem6  35764  subfacval2  35766  subfaclim  35767  cvxsconn  35822  resconn  35825  fwddifnp1  36745  itg2addnclem3  38422  itgmulc2nc  38437  rrnequiv  38585  aks4d1p1p7  42940  primrootscoprmpow  42965  3rdpwhole  43167  fltnlta  43509  cu3addd  43526  3cubeslem2  43530  3cubeslem3r  43532  jm2.19lem3  43832  jm2.25  43840  jm3.1lem2  43859  inductionexd  44995  int-leftdistd  45019  binomcxplemwb  45172  binomcxplemnotnn0  45180  sineq0ALT  45759  fperiodmullem  46136  xralrple2  46184  coskpi2  46694  cosknegpi  46697  dvnmul  46771  stoweidlem11  46839  stoweidlem13  46841  stirlinglem1  46902  stirlinglem4  46905  dirkerper  46924  dirkertrigeqlem1  46926  dirkertrigeqlem2  46927  dirkertrigeqlem3  46928  dirkercncflem2  46932  fourierdlem41  46976  fourierdlem42  46977  fourierdlem64  46998  fourierswlem  47058  hoidmvlelem2  47424  sigaraf  47681  sin3t  47735  cos3t  47736  sin5tlem1  47737  sin5tlem5  47741  sin5t  47742  cos5t  47743  fmtnorec3  48451  itscnhlc0yqe  49689  itsclc0yqsollem1  49692  itscnhlc0xyqsol  49695  itsclc0xyqsolr  49699  itsclquadb  49706  2itscplem3  49710  itscnhlinecirc02plem1  49712  crossp3d  50800