Theorem adddird 11140

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012   · cmul 11014

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 11069  ax-mulcom 11073  ax-distr 11076

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  adddirp1d  11141  joinlmuladdmuld  11142  addmulsub  11582  recextlem1  11750  divdir  11804  subsq  14117  subsq2  14118  binom3  14131  discr1  14146  cshweqrep  14727  remullem  15035  01sqrexlem7  15155  binomlem  15736  binomfallfaclem2  15947  pwp1fsum  16302  smumullem  16403  mul4sqlem  16865  vdwapun  16886  nn0srg  21344  rge0srg  21345  nmotri  24625  blcvx  24684  cphipval2  25139  itg1addlem5  25599  itgconst  25718  dvexp  25855  dvcvx  25923  plyaddlem1  26116  abelthlem7  26346  cxpadd  26586  dcubic  26754  binom4  26758  dquartlem2  26760  dquart  26761  quart1lem  26763  quart1  26764  cvxcl  26893  scvxcvx  26894  basellem9  26997  bposlem9  27201  lgsquad2lem1  27293  2sqlem4  27330  2sqblem  27340  dchrisumlem2  27399  dchrisum0lem1  27425  mudivsum  27439  chpdifbndlem1  27462  pntrlog2bndlem2  27487  pntlemr  27511  pntlemk  27515  ostth2lem2  27543  brbtwn2  28850  ax5seglem3  28876  ax5seglem5  28878  axbtwnid  28884  axeuclidlem  28907  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  ex-ind-dvds  30405  smcnlem  30641  ccfldsrarelvec  33638  constrrtll  33698  constrrtcclem  33701  constrrtcc  33702  cos9thpiminplylem2  33750  circlemeth  34608  hgt750lemd  34616  logdivsqrle  34618  subfacp1lem6  35158  subfacval2  35160  subfaclim  35161  cvxsconn  35216  resconn  35219  fwddifnp1  36139  itg2addnclem3  37653  itgmulc2nc  37668  rrnequiv  37815  aks4d1p1p7  42047  primrootscoprmpow  42072  3rdpwhole  42265  fltnlta  42636  cu3addd  42654  3cubeslem2  42658  3cubeslem3r  42660  jm2.19lem3  42964  jm2.25  42972  jm3.1lem2  42991  inductionexd  44128  int-leftdistd  44152  binomcxplemwb  44321  binomcxplemnotnn0  44329  sineq0ALT  44910  fperiodmullem  45285  xralrple2  45334  coskpi2  45847  cosknegpi  45850  dvnmul  45924  stoweidlem11  45992  stoweidlem13  45994  stirlinglem1  46055  stirlinglem4  46058  dirkerper  46077  dirkertrigeqlem1  46079  dirkertrigeqlem2  46080  dirkertrigeqlem3  46081  dirkercncflem2  46085  fourierdlem41  46129  fourierdlem42  46130  fourierdlem64  46151  fourierswlem  46211  hoidmvlelem2  46577  sigaraf  46834  fmtnorec3  47532  itscnhlc0yqe  48744  itsclc0yqsollem1  48747  itscnhlc0xyqsol  48750  itsclc0xyqsolr  48754  itsclquadb  48761  2itscplem3  48765  itscnhlinecirc02plem1  48767