Theorem adddird 10655

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-addcl 10586  ax-mulcom 10590  ax-distr 10593

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  adddirp1d  10656  joinlmuladdmuld  10657  addmulsub  11091  recextlem1  11259  divdir  11312  subsq  13568  subsq2  13569  binom3  13581  discr1  13596  cshweqrep  14174  remullem  14479  sqrlem7  14600  binomlem  15176  binomfallfaclem2  15386  pwp1fsum  15732  smumullem  15831  mul4sqlem  16279  vdwapun  16300  nn0srg  20161  rge0srg  20162  nmotri  23345  blcvx  23403  cphipval2  23845  itg1addlem5  24304  itgconst  24422  dvexp  24556  dvcvx  24623  plyaddlem1  24810  abelthlem7  25033  cxpadd  25270  dcubic  25432  binom4  25436  dquartlem2  25438  dquart  25439  quart1lem  25441  quart1  25442  cvxcl  25570  scvxcvx  25571  basellem9  25674  bposlem9  25876  lgsquad2lem1  25968  2sqlem4  26005  2sqblem  26015  dchrisumlem2  26074  dchrisum0lem1  26100  mudivsum  26114  chpdifbndlem1  26137  pntrlog2bndlem2  26162  pntlemr  26186  pntlemk  26190  ostth2lem2  26218  brbtwn2  26699  ax5seglem3  26725  ax5seglem5  26727  axbtwnid  26733  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  ex-ind-dvds  28246  smcnlem  28480  ccfldsrarelvec  31144  circlemeth  32021  hgt750lemd  32029  logdivsqrle  32031  subfacp1lem6  32545  subfacval2  32547  subfaclim  32548  cvxsconn  32603  resconn  32606  fwddifnp1  33739  itg2addnclem3  35110  itgmulc2nc  35125  rrnequiv  35273  fltnlta  39619  cu3addd  39621  3cubeslem2  39626  3cubeslem3r  39628  jm2.19lem3  39932  jm2.25  39940  jm3.1lem2  39959  inductionexd  40858  int-leftdistd  40885  binomcxplemwb  41052  binomcxplemnotnn0  41060  sineq0ALT  41643  fperiodmullem  41935  xralrple2  41986  coskpi2  42508  cosknegpi  42511  dvnmul  42585  stoweidlem11  42653  stoweidlem13  42655  stirlinglem1  42716  stirlinglem4  42719  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkercncflem2  42746  fourierdlem41  42790  fourierdlem42  42791  fourierdlem64  42812  fourierswlem  42872  hoidmvlelem2  43235  sigaraf  43467  fmtnorec3  44065  itscnhlc0yqe  45173  itsclc0yqsollem1  45176  itscnhlc0xyqsol  45179  itsclc0xyqsolr  45183  itsclquadb  45190  2itscplem3  45194  itscnhlinecirc02plem1  45196