Theorem adddird 11161

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   + caddc 11032   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-addcl 11089  ax-mulcom 11093  ax-distr 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  adddirp1d  11162  joinlmuladdmuld  11163  addmulsub  11603  recextlem1  11771  divdir  11825  subsq  14163  subsq2  14164  binom3  14177  discr1  14192  cshweqrep  14774  remullem  15081  01sqrexlem7  15201  binomlem  15785  binomfallfaclem2  15996  pwp1fsum  16351  smumullem  16452  mul4sqlem  16915  vdwapun  16936  nn0srg  21412  rge0srg  21413  nmotri  24722  blcvx  24781  cphipval2  25226  itg1addlem5  25685  itgconst  25804  dvexp  25938  dvcvx  26005  plyaddlem1  26196  abelthlem7  26421  cxpadd  26661  dcubic  26828  binom4  26832  dquartlem2  26834  dquart  26835  quart1lem  26837  quart1  26838  cvxcl  26966  scvxcvx  26967  basellem9  27070  bposlem9  27273  lgsquad2lem1  27365  2sqlem4  27402  2sqblem  27412  dchrisumlem2  27471  dchrisum0lem1  27497  mudivsum  27511  chpdifbndlem1  27534  pntrlog2bndlem2  27559  pntlemr  27583  pntlemk  27587  ostth2lem2  27615  brbtwn2  28992  ax5seglem3  29018  ax5seglem5  29020  axbtwnid  29026  axeuclidlem  29049  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  ex-ind-dvds  30549  smcnlem  30786  ccfldsrarelvec  33855  constrrtll  33915  constrrtcclem  33918  constrrtcc  33919  cos9thpiminplylem2  33967  circlemeth  34824  hgt750lemd  34832  logdivsqrle  34834  subfacp1lem6  35413  subfacval2  35415  subfaclim  35416  cvxsconn  35471  resconn  35474  fwddifnp1  36393  itg2addnclem3  38040  itgmulc2nc  38055  rrnequiv  38202  aks4d1p1p7  42559  primrootscoprmpow  42584  3rdpwhole  42769  fltnlta  43113  cu3addd  43130  3cubeslem2  43134  3cubeslem3r  43136  jm2.19lem3  43436  jm2.25  43444  jm3.1lem2  43463  inductionexd  44599  int-leftdistd  44623  binomcxplemwb  44792  binomcxplemnotnn0  44800  sineq0ALT  45380  fperiodmullem  45751  xralrple2  45799  coskpi2  46309  cosknegpi  46312  dvnmul  46386  stoweidlem11  46454  stoweidlem13  46456  stirlinglem1  46517  stirlinglem4  46520  dirkerper  46539  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkercncflem2  46547  fourierdlem41  46591  fourierdlem42  46592  fourierdlem64  46613  fourierswlem  46673  hoidmvlelem2  47039  sigaraf  47296  sin3t  47334  cos3t  47335  sin5tlem1  47336  sin5tlem5  47340  sin5t  47341  cos5t  47342  fmtnorec3  48026  itscnhlc0yqe  49250  itsclc0yqsollem1  49253  itscnhlc0xyqsol  49256  itsclc0xyqsolr  49260  itsclquadb  49267  2itscplem3  49271  itscnhlinecirc02plem1  49273