Theorem adddird 11249

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   + caddc 11118   · cmul 11120

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 2148  ax-9 2156  ax-ext 2737  ax-addcl 11175  ax-mulcom 11179  ax-distr 11182

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  adddirp1d  11250  joinlmuladdmuld  11251  addmulsub  11691  recextlem1  11859  divdir  11912  subsq  14264  subsq2  14265  binom3  14278  discr1  14293  cshweqrep  14882  remullem  15203  01sqrexlem7  15323  binomlem  15906  binomfallfaclem2  16116  pwp1fsum  16471  smumullem  16572  mul4sqlem  17035  vdwapun  17056  nn0srg  21637  rge0srg  21638  nmotri  24947  blcvx  25006  cphipval2  25451  itg1addlem5  25910  itgconst  26029  dvexp  26163  dvcvx  26230  plyaddlem1  26421  abelthlem7  26652  cxpadd  26895  dcubic  27062  binom4  27066  dquartlem2  27068  dquart  27069  quart1lem  27071  quart1  27072  cvxcl  27200  scvxcvx  27201  basellem9  27304  bposlem9  27507  lgsquad2lem1  27599  2sqlem4  27636  2sqblem  27646  dchrisumlem2  27705  dchrisum0lem1  27731  mudivsum  27745  chpdifbndlem1  27768  pntrlog2bndlem2  27793  pntlemr  27817  pntlemk  27821  ostth2lem2  27849  brbtwn2  29310  ax5seglem3  29336  ax5seglem5  29338  axbtwnid  29344  axeuclidlem  29367  axcontlem2  29370  axcontlem4  29372  axcontlem7  29375  ex-ind-dvds  30883  smcnlem  31120  ccfldsrarelvec  34125  constrrtll  34185  constrrtcclem  34188  constrrtcc  34189  cos9thpiminplylem2  34237  circlemeth  35092  hgt750lemd  35100  logdivsqrle  35102  subfacp1lem6  35714  subfacval2  35716  subfaclim  35717  cvxsconn  35772  resconn  35775  fwddifnp1  36694  itg2addnclem3  38381  itgmulc2nc  38396  rrnequiv  38544  aks4d1p1p7  42899  primrootscoprmpow  42924  3rdpwhole  43111  fltnlta  43453  cu3addd  43470  3cubeslem2  43474  3cubeslem3r  43476  jm2.19lem3  43776  jm2.25  43784  jm3.1lem2  43803  inductionexd  44939  int-leftdistd  44963  binomcxplemwb  45116  binomcxplemnotnn0  45124  sineq0ALT  45703  fperiodmullem  46080  xralrple2  46128  coskpi2  46638  cosknegpi  46641  dvnmul  46715  stoweidlem11  46783  stoweidlem13  46785  stirlinglem1  46846  stirlinglem4  46849  dirkerper  46868  dirkertrigeqlem1  46870  dirkertrigeqlem2  46871  dirkertrigeqlem3  46872  dirkercncflem2  46876  fourierdlem41  46920  fourierdlem42  46921  fourierdlem64  46942  fourierswlem  47002  hoidmvlelem2  47368  sigaraf  47625  sin3t  47666  cos3t  47667  sin5tlem1  47668  sin5tlem5  47672  sin5t  47673  cos5t  47674  fmtnorec3  48358  itscnhlc0yqe  49596  itsclc0yqsollem1  49599  itscnhlc0xyqsol  49602  itsclc0xyqsolr  49606  itsclquadb  49613  2itscplem3  49617  itscnhlinecirc02plem1  49619  crossp3d  50706