Theorem adddird 11157

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-addcl 11086  ax-mulcom 11090  ax-distr 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  adddirp1d  11158  joinlmuladdmuld  11159  addmulsub  11599  recextlem1  11767  divdir  11821  subsq  14133  subsq2  14134  binom3  14147  discr1  14162  cshweqrep  14744  remullem  15051  01sqrexlem7  15171  binomlem  15752  binomfallfaclem2  15963  pwp1fsum  16318  smumullem  16419  mul4sqlem  16881  vdwapun  16902  nn0srg  21392  rge0srg  21393  nmotri  24683  blcvx  24742  cphipval2  25197  itg1addlem5  25657  itgconst  25776  dvexp  25913  dvcvx  25981  plyaddlem1  26174  abelthlem7  26404  cxpadd  26644  dcubic  26812  binom4  26816  dquartlem2  26818  dquart  26819  quart1lem  26821  quart1  26822  cvxcl  26951  scvxcvx  26952  basellem9  27055  bposlem9  27259  lgsquad2lem1  27351  2sqlem4  27388  2sqblem  27398  dchrisumlem2  27457  dchrisum0lem1  27483  mudivsum  27497  chpdifbndlem1  27520  pntrlog2bndlem2  27545  pntlemr  27569  pntlemk  27573  ostth2lem2  27601  brbtwn2  28978  ax5seglem3  29004  ax5seglem5  29006  axbtwnid  29012  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  ex-ind-dvds  30536  smcnlem  30772  ccfldsrarelvec  33828  constrrtll  33888  constrrtcclem  33891  constrrtcc  33892  cos9thpiminplylem2  33940  circlemeth  34797  hgt750lemd  34805  logdivsqrle  34807  subfacp1lem6  35379  subfacval2  35381  subfaclim  35382  cvxsconn  35437  resconn  35440  fwddifnp1  36359  itg2addnclem3  37874  itgmulc2nc  37889  rrnequiv  38036  aks4d1p1p7  42328  primrootscoprmpow  42353  3rdpwhole  42547  fltnlta  42906  cu3addd  42923  3cubeslem2  42927  3cubeslem3r  42929  jm2.19lem3  43233  jm2.25  43241  jm3.1lem2  43260  inductionexd  44396  int-leftdistd  44420  binomcxplemwb  44589  binomcxplemnotnn0  44597  sineq0ALT  45177  fperiodmullem  45551  xralrple2  45599  coskpi2  46110  cosknegpi  46113  dvnmul  46187  stoweidlem11  46255  stoweidlem13  46257  stirlinglem1  46318  stirlinglem4  46321  dirkerper  46340  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkercncflem2  46348  fourierdlem41  46392  fourierdlem42  46393  fourierdlem64  46414  fourierswlem  46474  hoidmvlelem2  46840  sigaraf  47097  fmtnorec3  47794  itscnhlc0yqe  49005  itsclc0yqsollem1  49008  itscnhlc0xyqsol  49011  itsclc0xyqsolr  49015  itsclquadb  49022  2itscplem3  49026  itscnhlinecirc02plem1  49028