Theorem adddird 11148

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015   + caddc 11020   · cmul 11022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-addcl 11077  ax-mulcom 11081  ax-distr 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358

This theorem is referenced by:  adddirp1d  11149  joinlmuladdmuld  11150  addmulsub  11590  recextlem1  11758  divdir  11812  subsq  14124  subsq2  14125  binom3  14138  discr1  14153  cshweqrep  14735  remullem  15042  01sqrexlem7  15162  binomlem  15743  binomfallfaclem2  15954  pwp1fsum  16309  smumullem  16410  mul4sqlem  16872  vdwapun  16893  nn0srg  21383  rge0srg  21384  nmotri  24674  blcvx  24733  cphipval2  25188  itg1addlem5  25648  itgconst  25767  dvexp  25904  dvcvx  25972  plyaddlem1  26165  abelthlem7  26395  cxpadd  26635  dcubic  26803  binom4  26807  dquartlem2  26809  dquart  26810  quart1lem  26812  quart1  26813  cvxcl  26942  scvxcvx  26943  basellem9  27046  bposlem9  27250  lgsquad2lem1  27342  2sqlem4  27379  2sqblem  27389  dchrisumlem2  27448  dchrisum0lem1  27474  mudivsum  27488  chpdifbndlem1  27511  pntrlog2bndlem2  27536  pntlemr  27560  pntlemk  27564  ostth2lem2  27592  brbtwn2  28904  ax5seglem3  28930  ax5seglem5  28932  axbtwnid  28938  axeuclidlem  28961  axcontlem2  28964  axcontlem4  28966  axcontlem7  28969  ex-ind-dvds  30462  smcnlem  30698  ccfldsrarelvec  33756  constrrtll  33816  constrrtcclem  33819  constrrtcc  33820  cos9thpiminplylem2  33868  circlemeth  34725  hgt750lemd  34733  logdivsqrle  34735  subfacp1lem6  35301  subfacval2  35303  subfaclim  35304  cvxsconn  35359  resconn  35362  fwddifnp1  36281  itg2addnclem3  37786  itgmulc2nc  37801  rrnequiv  37948  aks4d1p1p7  42240  primrootscoprmpow  42265  3rdpwhole  42462  fltnlta  42821  cu3addd  42838  3cubeslem2  42842  3cubeslem3r  42844  jm2.19lem3  43148  jm2.25  43156  jm3.1lem2  43175  inductionexd  44312  int-leftdistd  44336  binomcxplemwb  44505  binomcxplemnotnn0  44513  sineq0ALT  45093  fperiodmullem  45467  xralrple2  45515  coskpi2  46026  cosknegpi  46029  dvnmul  46103  stoweidlem11  46171  stoweidlem13  46173  stirlinglem1  46234  stirlinglem4  46237  dirkerper  46256  dirkertrigeqlem1  46258  dirkertrigeqlem2  46259  dirkertrigeqlem3  46260  dirkercncflem2  46264  fourierdlem41  46308  fourierdlem42  46309  fourierdlem64  46330  fourierswlem  46390  hoidmvlelem2  46756  sigaraf  47013  fmtnorec3  47710  itscnhlc0yqe  48921  itsclc0yqsollem1  48924  itscnhlc0xyqsol  48927  itsclc0xyqsolr  48931  itsclquadb  48938  2itscplem3  48942  itscnhlinecirc02plem1  48944