Theorem adddird 11201

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7391  ℂcc 11065   + caddc 11070   · cmul 11072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-addcl 11127  ax-mulcom 11131  ax-distr 11134

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394

This theorem is referenced by:  adddirp1d  11202  joinlmuladdmuld  11203  addmulsub  11643  recextlem1  11811  divdir  11864  subsq  14217  subsq2  14218  binom3  14231  discr1  14246  cshweqrep  14828  remullem  15146  01sqrexlem7  15266  binomlem  15850  binomfallfaclem2  16061  pwp1fsum  16416  smumullem  16517  mul4sqlem  16980  vdwapun  17001  nn0srg  21477  rge0srg  21478  nmotri  24787  blcvx  24846  cphipval2  25291  itg1addlem5  25750  itgconst  25869  dvexp  26003  dvcvx  26070  plyaddlem1  26261  abelthlem7  26489  cxpadd  26732  dcubic  26899  binom4  26903  dquartlem2  26905  dquart  26906  quart1lem  26908  quart1  26909  cvxcl  27037  scvxcvx  27038  basellem9  27141  bposlem9  27344  lgsquad2lem1  27436  2sqlem4  27473  2sqblem  27483  dchrisumlem2  27542  dchrisum0lem1  27568  mudivsum  27582  chpdifbndlem1  27605  pntrlog2bndlem2  27630  pntlemr  27654  pntlemk  27658  ostth2lem2  27686  brbtwn2  29063  ax5seglem3  29089  ax5seglem5  29091  axbtwnid  29097  axeuclidlem  29120  axcontlem2  29123  axcontlem4  29125  axcontlem7  29128  ex-ind-dvds  30620  smcnlem  30857  ccfldsrarelvec  33929  constrrtll  33989  constrrtcclem  33992  constrrtcc  33993  cos9thpiminplylem2  34041  circlemeth  34895  hgt750lemd  34903  logdivsqrle  34905  subfacp1lem6  35496  subfacval2  35498  subfaclim  35499  cvxsconn  35554  resconn  35557  fwddifnp1  36476  itg2addnclem3  38133  itgmulc2nc  38148  rrnequiv  38295  aks4d1p1p7  42652  primrootscoprmpow  42677  3rdpwhole  42862  fltnlta  43206  cu3addd  43223  3cubeslem2  43227  3cubeslem3r  43229  jm2.19lem3  43529  jm2.25  43537  jm3.1lem2  43556  inductionexd  44692  int-leftdistd  44716  binomcxplemwb  44885  binomcxplemnotnn0  44893  sineq0ALT  45473  fperiodmullem  45843  xralrple2  45891  coskpi2  46401  cosknegpi  46404  dvnmul  46478  stoweidlem11  46546  stoweidlem13  46548  stirlinglem1  46609  stirlinglem4  46612  dirkerper  46631  dirkertrigeqlem1  46633  dirkertrigeqlem2  46634  dirkertrigeqlem3  46635  dirkercncflem2  46639  fourierdlem41  46683  fourierdlem42  46684  fourierdlem64  46705  fourierswlem  46765  hoidmvlelem2  47131  sigaraf  47388  sin3t  47426  cos3t  47427  sin5tlem1  47428  sin5tlem5  47432  sin5t  47433  cos5t  47434  fmtnorec3  48118  itscnhlc0yqe  49342  itsclc0yqsollem1  49345  itscnhlc0xyqsol  49348  itsclc0xyqsolr  49352  itsclquadb  49359  2itscplem3  49363  itscnhlinecirc02plem1  49365