Theorem adddird 11175

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047   · cmul 11049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-addcl 11104  ax-mulcom 11108  ax-distr 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  adddirp1d  11176  joinlmuladdmuld  11177  addmulsub  11616  recextlem1  11784  divdir  11838  subsq  14151  subsq2  14152  binom3  14165  discr1  14180  cshweqrep  14762  remullem  15070  01sqrexlem7  15190  binomlem  15771  binomfallfaclem2  15982  pwp1fsum  16337  smumullem  16438  mul4sqlem  16900  vdwapun  16921  nn0srg  21330  rge0srg  21331  nmotri  24603  blcvx  24662  cphipval2  25117  itg1addlem5  25577  itgconst  25696  dvexp  25833  dvcvx  25901  plyaddlem1  26094  abelthlem7  26324  cxpadd  26564  dcubic  26732  binom4  26736  dquartlem2  26738  dquart  26739  quart1lem  26741  quart1  26742  cvxcl  26871  scvxcvx  26872  basellem9  26975  bposlem9  27179  lgsquad2lem1  27271  2sqlem4  27308  2sqblem  27318  dchrisumlem2  27377  dchrisum0lem1  27403  mudivsum  27417  chpdifbndlem1  27440  pntrlog2bndlem2  27465  pntlemr  27489  pntlemk  27493  ostth2lem2  27521  brbtwn2  28808  ax5seglem3  28834  ax5seglem5  28836  axbtwnid  28842  axeuclidlem  28865  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  ex-ind-dvds  30363  smcnlem  30599  ccfldsrarelvec  33639  constrrtll  33694  constrrtcclem  33697  constrrtcc  33698  cos9thpiminplylem2  33746  circlemeth  34604  hgt750lemd  34612  logdivsqrle  34614  subfacp1lem6  35145  subfacval2  35147  subfaclim  35148  cvxsconn  35203  resconn  35206  fwddifnp1  36126  itg2addnclem3  37640  itgmulc2nc  37655  rrnequiv  37802  aks4d1p1p7  42035  primrootscoprmpow  42060  3rdpwhole  42253  fltnlta  42624  cu3addd  42642  3cubeslem2  42646  3cubeslem3r  42648  jm2.19lem3  42953  jm2.25  42961  jm3.1lem2  42980  inductionexd  44117  int-leftdistd  44141  binomcxplemwb  44310  binomcxplemnotnn0  44318  sineq0ALT  44899  fperiodmullem  45274  xralrple2  45323  coskpi2  45837  cosknegpi  45840  dvnmul  45914  stoweidlem11  45982  stoweidlem13  45984  stirlinglem1  46045  stirlinglem4  46048  dirkerper  46067  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkercncflem2  46075  fourierdlem41  46119  fourierdlem42  46120  fourierdlem64  46141  fourierswlem  46201  hoidmvlelem2  46567  sigaraf  46824  fmtnorec3  47522  itscnhlc0yqe  48721  itsclc0yqsollem1  48724  itscnhlc0xyqsol  48727  itsclc0xyqsolr  48731  itsclquadb  48738  2itscplem3  48742  itscnhlinecirc02plem1  48744