Theorem adddird 11206

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   · cmul 11080

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 2702  ax-addcl 11135  ax-mulcom 11139  ax-distr 11142

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  adddirp1d  11207  joinlmuladdmuld  11208  addmulsub  11647  recextlem1  11815  divdir  11869  subsq  14182  subsq2  14183  binom3  14196  discr1  14211  cshweqrep  14793  remullem  15101  01sqrexlem7  15221  binomlem  15802  binomfallfaclem2  16013  pwp1fsum  16368  smumullem  16469  mul4sqlem  16931  vdwapun  16952  nn0srg  21361  rge0srg  21362  nmotri  24634  blcvx  24693  cphipval2  25148  itg1addlem5  25608  itgconst  25727  dvexp  25864  dvcvx  25932  plyaddlem1  26125  abelthlem7  26355  cxpadd  26595  dcubic  26763  binom4  26767  dquartlem2  26769  dquart  26770  quart1lem  26772  quart1  26773  cvxcl  26902  scvxcvx  26903  basellem9  27006  bposlem9  27210  lgsquad2lem1  27302  2sqlem4  27339  2sqblem  27349  dchrisumlem2  27408  dchrisum0lem1  27434  mudivsum  27448  chpdifbndlem1  27471  pntrlog2bndlem2  27496  pntlemr  27520  pntlemk  27524  ostth2lem2  27552  brbtwn2  28839  ax5seglem3  28865  ax5seglem5  28867  axbtwnid  28873  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  ex-ind-dvds  30397  smcnlem  30633  ccfldsrarelvec  33673  constrrtll  33728  constrrtcclem  33731  constrrtcc  33732  cos9thpiminplylem2  33780  circlemeth  34638  hgt750lemd  34646  logdivsqrle  34648  subfacp1lem6  35179  subfacval2  35181  subfaclim  35182  cvxsconn  35237  resconn  35240  fwddifnp1  36160  itg2addnclem3  37674  itgmulc2nc  37689  rrnequiv  37836  aks4d1p1p7  42069  primrootscoprmpow  42094  3rdpwhole  42287  fltnlta  42658  cu3addd  42676  3cubeslem2  42680  3cubeslem3r  42682  jm2.19lem3  42987  jm2.25  42995  jm3.1lem2  43014  inductionexd  44151  int-leftdistd  44175  binomcxplemwb  44344  binomcxplemnotnn0  44352  sineq0ALT  44933  fperiodmullem  45308  xralrple2  45357  coskpi2  45871  cosknegpi  45874  dvnmul  45948  stoweidlem11  46016  stoweidlem13  46018  stirlinglem1  46079  stirlinglem4  46082  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem41  46153  fourierdlem42  46154  fourierdlem64  46175  fourierswlem  46235  hoidmvlelem2  46601  sigaraf  46858  fmtnorec3  47553  itscnhlc0yqe  48752  itsclc0yqsollem1  48755  itscnhlc0xyqsol  48758  itsclc0xyqsolr  48762  itsclquadb  48769  2itscplem3  48773  itscnhlinecirc02plem1  48775