Theorem adddird 11046

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   + caddc 10920   · cmul 10922

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-addcl 10977  ax-mulcom 10981  ax-distr 10984

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310

This theorem is referenced by:  adddirp1d  11047  joinlmuladdmuld  11048  addmulsub  11483  recextlem1  11651  divdir  11704  subsq  13972  subsq2  13973  binom3  13985  discr1  14000  cshweqrep  14579  remullem  14884  sqrlem7  15005  binomlem  15586  binomfallfaclem2  15795  pwp1fsum  16145  smumullem  16244  mul4sqlem  16699  vdwapun  16720  nn0srg  20713  rge0srg  20714  nmotri  23948  blcvx  24006  cphipval2  24450  itg1addlem5  24910  itgconst  25028  dvexp  25162  dvcvx  25229  plyaddlem1  25419  abelthlem7  25642  cxpadd  25879  dcubic  26041  binom4  26045  dquartlem2  26047  dquart  26048  quart1lem  26050  quart1  26051  cvxcl  26179  scvxcvx  26180  basellem9  26283  bposlem9  26485  lgsquad2lem1  26577  2sqlem4  26614  2sqblem  26624  dchrisumlem2  26683  dchrisum0lem1  26709  mudivsum  26723  chpdifbndlem1  26746  pntrlog2bndlem2  26771  pntlemr  26795  pntlemk  26799  ostth2lem2  26827  brbtwn2  27318  ax5seglem3  27344  ax5seglem5  27346  axbtwnid  27352  axeuclidlem  27375  axcontlem2  27378  axcontlem4  27380  axcontlem7  27383  ex-ind-dvds  28870  smcnlem  29104  ccfldsrarelvec  31786  circlemeth  32665  hgt750lemd  32673  logdivsqrle  32675  subfacp1lem6  33192  subfacval2  33194  subfaclim  33195  cvxsconn  33250  resconn  33253  fwddifnp1  34512  itg2addnclem3  35874  itgmulc2nc  35889  rrnequiv  36037  aks4d1p1p7  40124  fltnlta  40537  cu3addd  40539  3cubeslem2  40544  3cubeslem3r  40546  jm2.19lem3  40851  jm2.25  40859  jm3.1lem2  40878  inductionexd  41803  int-leftdistd  41828  binomcxplemwb  42004  binomcxplemnotnn0  42012  sineq0ALT  42595  fperiodmullem  42890  xralrple2  42941  coskpi2  43456  cosknegpi  43459  dvnmul  43533  stoweidlem11  43601  stoweidlem13  43603  stirlinglem1  43664  stirlinglem4  43667  dirkerper  43686  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkertrigeqlem3  43690  dirkercncflem2  43694  fourierdlem41  43738  fourierdlem42  43739  fourierdlem64  43760  fourierswlem  43820  hoidmvlelem2  44184  sigaraf  44427  fmtnorec3  45058  itscnhlc0yqe  46163  itsclc0yqsollem1  46166  itscnhlc0xyqsol  46169  itsclc0xyqsolr  46173  itsclquadb  46180  2itscplem3  46184  itscnhlinecirc02plem1  46186