Theorem adddird 11243

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   + caddc 11115   · cmul 11117

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 2701  ax-addcl 11172  ax-mulcom 11176  ax-distr 11179

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  adddirp1d  11244  joinlmuladdmuld  11245  addmulsub  11680  recextlem1  11848  divdir  11901  subsq  14178  subsq2  14179  binom3  14191  discr1  14206  cshweqrep  14775  remullem  15079  01sqrexlem7  15199  binomlem  15779  binomfallfaclem2  15988  pwp1fsum  16338  smumullem  16437  mul4sqlem  16890  vdwapun  16911  nn0srg  21215  rge0srg  21216  nmotri  24476  blcvx  24534  cphipval2  24989  itg1addlem5  25450  itgconst  25568  dvexp  25705  dvcvx  25772  plyaddlem1  25962  abelthlem7  26186  cxpadd  26423  dcubic  26587  binom4  26591  dquartlem2  26593  dquart  26594  quart1lem  26596  quart1  26597  cvxcl  26725  scvxcvx  26726  basellem9  26829  bposlem9  27031  lgsquad2lem1  27123  2sqlem4  27160  2sqblem  27170  dchrisumlem2  27229  dchrisum0lem1  27255  mudivsum  27269  chpdifbndlem1  27292  pntrlog2bndlem2  27317  pntlemr  27341  pntlemk  27345  ostth2lem2  27373  brbtwn2  28430  ax5seglem3  28456  ax5seglem5  28458  axbtwnid  28464  axeuclidlem  28487  axcontlem2  28490  axcontlem4  28492  axcontlem7  28495  ex-ind-dvds  29981  smcnlem  30217  ccfldsrarelvec  33034  circlemeth  33950  hgt750lemd  33958  logdivsqrle  33960  subfacp1lem6  34474  subfacval2  34476  subfaclim  34477  cvxsconn  34532  resconn  34535  fwddifnp1  35441  itg2addnclem3  36844  itgmulc2nc  36859  rrnequiv  37006  aks4d1p1p7  41245  fltnlta  41707  cu3addd  41720  3cubeslem2  41725  3cubeslem3r  41727  jm2.19lem3  42032  jm2.25  42040  jm3.1lem2  42059  inductionexd  43208  int-leftdistd  43233  binomcxplemwb  43409  binomcxplemnotnn0  43417  sineq0ALT  44000  fperiodmullem  44311  xralrple2  44362  coskpi2  44880  cosknegpi  44883  dvnmul  44957  stoweidlem11  45025  stoweidlem13  45027  stirlinglem1  45088  stirlinglem4  45091  dirkerper  45110  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkertrigeqlem3  45114  dirkercncflem2  45118  fourierdlem41  45162  fourierdlem42  45163  fourierdlem64  45184  fourierswlem  45244  hoidmvlelem2  45610  sigaraf  45867  fmtnorec3  46514  itscnhlc0yqe  47532  itsclc0yqsollem1  47535  itscnhlc0xyqsol  47538  itsclc0xyqsolr  47542  itsclquadb  47549  2itscplem3  47553  itscnhlinecirc02plem1  47555