Theorem adddird 10984

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858   · cmul 10860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-addcl 10915  ax-mulcom 10919  ax-distr 10922

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  adddirp1d  10985  joinlmuladdmuld  10986  addmulsub  11420  recextlem1  11588  divdir  11641  subsq  13907  subsq2  13908  binom3  13920  discr1  13935  cshweqrep  14515  remullem  14820  sqrlem7  14941  binomlem  15522  binomfallfaclem2  15731  pwp1fsum  16081  smumullem  16180  mul4sqlem  16635  vdwapun  16656  nn0srg  20649  rge0srg  20650  nmotri  23884  blcvx  23942  cphipval2  24386  itg1addlem5  24846  itgconst  24964  dvexp  25098  dvcvx  25165  plyaddlem1  25355  abelthlem7  25578  cxpadd  25815  dcubic  25977  binom4  25981  dquartlem2  25983  dquart  25984  quart1lem  25986  quart1  25987  cvxcl  26115  scvxcvx  26116  basellem9  26219  bposlem9  26421  lgsquad2lem1  26513  2sqlem4  26550  2sqblem  26560  dchrisumlem2  26619  dchrisum0lem1  26645  mudivsum  26659  chpdifbndlem1  26682  pntrlog2bndlem2  26707  pntlemr  26731  pntlemk  26735  ostth2lem2  26763  brbtwn2  27254  ax5seglem3  27280  ax5seglem5  27282  axbtwnid  27288  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  ex-ind-dvds  28804  smcnlem  29038  ccfldsrarelvec  31720  circlemeth  32599  hgt750lemd  32607  logdivsqrle  32609  subfacp1lem6  33126  subfacval2  33128  subfaclim  33129  cvxsconn  33184  resconn  33187  fwddifnp1  34446  itg2addnclem3  35809  itgmulc2nc  35824  rrnequiv  35972  aks4d1p1p7  40062  fltnlta  40480  cu3addd  40482  3cubeslem2  40487  3cubeslem3r  40489  jm2.19lem3  40793  jm2.25  40801  jm3.1lem2  40820  inductionexd  41718  int-leftdistd  41743  binomcxplemwb  41919  binomcxplemnotnn0  41927  sineq0ALT  42510  fperiodmullem  42796  xralrple2  42847  coskpi2  43361  cosknegpi  43364  dvnmul  43438  stoweidlem11  43506  stoweidlem13  43508  stirlinglem1  43569  stirlinglem4  43572  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  dirkercncflem2  43599  fourierdlem41  43643  fourierdlem42  43644  fourierdlem64  43665  fourierswlem  43725  hoidmvlelem2  44088  sigaraf  44320  fmtnorec3  44952  itscnhlc0yqe  46057  itsclc0yqsollem1  46060  itscnhlc0xyqsol  46063  itsclc0xyqsolr  46067  itsclquadb  46074  2itscplem3  46078  itscnhlinecirc02plem1  46080