Theorem adddird 11233

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11097   + caddc 11102   · cmul 11104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-addcl 11159  ax-mulcom 11163  ax-distr 11166

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  adddirp1d  11234  joinlmuladdmuld  11235  addmulsub  11675  recextlem1  11843  divdir  11896  subsq  14245  subsq2  14246  binom3  14259  discr1  14274  cshweqrep  14857  remullem  15178  01sqrexlem7  15298  binomlem  15882  binomfallfaclem2  16093  pwp1fsum  16448  smumullem  16549  mul4sqlem  17012  vdwapun  17033  nn0srg  21555  rge0srg  21556  nmotri  24864  blcvx  24923  cphipval2  25368  itg1addlem5  25827  itgconst  25946  dvexp  26080  dvcvx  26147  plyaddlem1  26338  abelthlem7  26566  cxpadd  26809  dcubic  26976  binom4  26980  dquartlem2  26982  dquart  26983  quart1lem  26985  quart1  26986  cvxcl  27114  scvxcvx  27115  basellem9  27218  bposlem9  27421  lgsquad2lem1  27513  2sqlem4  27550  2sqblem  27560  dchrisumlem2  27619  dchrisum0lem1  27645  mudivsum  27659  chpdifbndlem1  27682  pntrlog2bndlem2  27707  pntlemr  27731  pntlemk  27735  ostth2lem2  27763  brbtwn2  29195  ax5seglem3  29221  ax5seglem5  29223  axbtwnid  29229  axeuclidlem  29252  axcontlem2  29255  axcontlem4  29257  axcontlem7  29260  ex-ind-dvds  30752  smcnlem  30989  ccfldsrarelvec  34005  constrrtll  34065  constrrtcclem  34068  constrrtcc  34069  cos9thpiminplylem2  34117  circlemeth  34971  hgt750lemd  34979  logdivsqrle  34981  subfacp1lem6  35575  subfacval2  35577  subfaclim  35578  cvxsconn  35633  resconn  35636  fwddifnp1  36555  itg2addnclem3  38211  itgmulc2nc  38226  rrnequiv  38373  aks4d1p1p7  42730  primrootscoprmpow  42755  3rdpwhole  42942  fltnlta  43286  cu3addd  43303  3cubeslem2  43307  3cubeslem3r  43309  jm2.19lem3  43609  jm2.25  43617  jm3.1lem2  43636  inductionexd  44772  int-leftdistd  44796  binomcxplemwb  44949  binomcxplemnotnn0  44957  sineq0ALT  45536  fperiodmullem  45913  xralrple2  45961  coskpi2  46471  cosknegpi  46474  dvnmul  46548  stoweidlem11  46616  stoweidlem13  46618  stirlinglem1  46679  stirlinglem4  46682  dirkerper  46701  dirkertrigeqlem1  46703  dirkertrigeqlem2  46704  dirkertrigeqlem3  46705  dirkercncflem2  46709  fourierdlem41  46753  fourierdlem42  46754  fourierdlem64  46775  fourierswlem  46835  hoidmvlelem2  47201  sigaraf  47458  sin3t  47496  cos3t  47497  sin5tlem1  47498  sin5tlem5  47502  sin5t  47503  cos5t  47504  fmtnorec3  48188  itscnhlc0yqe  49423  itsclc0yqsollem1  49426  itscnhlc0xyqsol  49429  itsclc0xyqsolr  49433  itsclquadb  49440  2itscplem3  49444  itscnhlinecirc02plem1  49446