Theorem adddird 9944

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-addcl 9875  ax-mulcom 9879  ax-distr 9882

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  adddirp1d  9945  joinlmuladdmuld  9946  1p1times  10086  recextlem1  10536  divdir  10589  ltdifltdiv  12497  modvalp1  12551  subsq  12834  subsq2  12835  binom3  12847  discr1  12862  cshweqrep  13418  remullem  13716  sqrlem7  13837  binomlem  14400  arisum  14431  binomfallfaclem2  14610  pwp1fsum  14952  smumullem  15052  bezoutlem3  15096  bezoutlem4  15097  pcexp  15402  mul4sqlem  15495  vdwapun  15516  mulgnnass  17399  mulgnnassOLD  17400  cnfldmulg  19597  nn0srg  19635  rge0srg  19636  nmotri  22353  blcvx  22409  cphipval2  22848  itg1addlem5  23273  mbfi1fseqlem4  23291  itgconst  23391  itgmulc2  23406  dvexp  23522  dvcvx  23587  plyaddlem1  23773  dgrcolem1  23833  abelthlem2  23990  abelthlem7  23996  tangtx  24061  cxpadd  24225  dcubic  24373  binom4  24377  dquartlem2  24379  dquart  24380  quart1lem  24382  quart1  24383  cvxcl  24511  scvxcvx  24512  basellem9  24615  bposlem9  24817  lgsquad2lem1  24909  2sqlem4  24946  2sqblem  24956  dchrisumlem2  24979  dchrisum0lem1  25005  mudivsum  25019  chpdifbndlem1  25042  pntrlog2bndlem2  25067  pntlemr  25091  pntlemk  25095  ostth2lem2  25123  brbtwn2  25585  ax5seglem3  25611  ax5seglem5  25613  axbtwnid  25619  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  ex-ind-dvds  26710  smcnlem  26936  subfacp1lem6  30421  subfacval2  30423  subfaclim  30424  cvxscon  30479  rescon  30482  fwddifnp1  31442  itg2addnclem3  32633  itgmulc2nc  32648  rrnequiv  32804  jm2.19lem3  36576  jm2.25  36584  jm3.1lem2  36603  inductionexd  37473  int-leftdistd  37504  int-rightdistd  37505  binomcxplemwb  37569  binomcxplemnotnn0  37577  sineq0ALT  38195  fperiodmullem  38458  xralrple2  38511  coskpi2  38749  cosknegpi  38752  dvnmul  38833  stoweidlem11  38904  stoweidlem13  38906  stirlinglem1  38967  stirlinglem4  38970  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkercncflem2  38997  fourierdlem41  39041  fourierdlem42  39042  fourierdlem64  39063  fourierswlem  39123  hoidmvlelem2  39486  sigaraf  39691  fmtnorec3  39998