Theorem adddird 11199

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   · cmul 11073

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-addcl 11128  ax-mulcom 11132  ax-distr 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  adddirp1d  11200  joinlmuladdmuld  11201  addmulsub  11640  recextlem1  11808  divdir  11862  subsq  14175  subsq2  14176  binom3  14189  discr1  14204  cshweqrep  14786  remullem  15094  01sqrexlem7  15214  binomlem  15795  binomfallfaclem2  16006  pwp1fsum  16361  smumullem  16462  mul4sqlem  16924  vdwapun  16945  nn0srg  21354  rge0srg  21355  nmotri  24627  blcvx  24686  cphipval2  25141  itg1addlem5  25601  itgconst  25720  dvexp  25857  dvcvx  25925  plyaddlem1  26118  abelthlem7  26348  cxpadd  26588  dcubic  26756  binom4  26760  dquartlem2  26762  dquart  26763  quart1lem  26765  quart1  26766  cvxcl  26895  scvxcvx  26896  basellem9  26999  bposlem9  27203  lgsquad2lem1  27295  2sqlem4  27332  2sqblem  27342  dchrisumlem2  27401  dchrisum0lem1  27427  mudivsum  27441  chpdifbndlem1  27464  pntrlog2bndlem2  27489  pntlemr  27513  pntlemk  27517  ostth2lem2  27545  brbtwn2  28832  ax5seglem3  28858  ax5seglem5  28860  axbtwnid  28866  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  ex-ind-dvds  30390  smcnlem  30626  ccfldsrarelvec  33666  constrrtll  33721  constrrtcclem  33724  constrrtcc  33725  cos9thpiminplylem2  33773  circlemeth  34631  hgt750lemd  34639  logdivsqrle  34641  subfacp1lem6  35172  subfacval2  35174  subfaclim  35175  cvxsconn  35230  resconn  35233  fwddifnp1  36153  itg2addnclem3  37667  itgmulc2nc  37682  rrnequiv  37829  aks4d1p1p7  42062  primrootscoprmpow  42087  3rdpwhole  42280  fltnlta  42651  cu3addd  42669  3cubeslem2  42673  3cubeslem3r  42675  jm2.19lem3  42980  jm2.25  42988  jm3.1lem2  43007  inductionexd  44144  int-leftdistd  44168  binomcxplemwb  44337  binomcxplemnotnn0  44345  sineq0ALT  44926  fperiodmullem  45301  xralrple2  45350  coskpi2  45864  cosknegpi  45867  dvnmul  45941  stoweidlem11  46009  stoweidlem13  46011  stirlinglem1  46072  stirlinglem4  46075  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem2  46102  fourierdlem41  46146  fourierdlem42  46147  fourierdlem64  46168  fourierswlem  46228  hoidmvlelem2  46594  sigaraf  46851  fmtnorec3  47549  itscnhlc0yqe  48748  itsclc0yqsollem1  48751  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itsclquadb  48765  2itscplem3  48769  itscnhlinecirc02plem1  48771