Theorem adddird 11001

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  (class class class)co 7271  ℂcc 10870   + caddc 10875   · cmul 10877

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-addcl 10932  ax-mulcom 10936  ax-distr 10939

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6390  df-fv 6440  df-ov 7274

This theorem is referenced by:  adddirp1d  11002  joinlmuladdmuld  11003  addmulsub  11437  recextlem1  11605  divdir  11658  subsq  13924  subsq2  13925  binom3  13937  discr1  13952  cshweqrep  14532  remullem  14837  sqrlem7  14958  binomlem  15539  binomfallfaclem2  15748  pwp1fsum  16098  smumullem  16197  mul4sqlem  16652  vdwapun  16673  nn0srg  20666  rge0srg  20667  nmotri  23901  blcvx  23959  cphipval2  24403  itg1addlem5  24863  itgconst  24981  dvexp  25115  dvcvx  25182  plyaddlem1  25372  abelthlem7  25595  cxpadd  25832  dcubic  25994  binom4  25998  dquartlem2  26000  dquart  26001  quart1lem  26003  quart1  26004  cvxcl  26132  scvxcvx  26133  basellem9  26236  bposlem9  26438  lgsquad2lem1  26530  2sqlem4  26567  2sqblem  26577  dchrisumlem2  26636  dchrisum0lem1  26662  mudivsum  26676  chpdifbndlem1  26699  pntrlog2bndlem2  26724  pntlemr  26748  pntlemk  26752  ostth2lem2  26780  brbtwn2  27271  ax5seglem3  27297  ax5seglem5  27299  axbtwnid  27305  axeuclidlem  27328  axcontlem2  27331  axcontlem4  27333  axcontlem7  27336  ex-ind-dvds  28821  smcnlem  29055  ccfldsrarelvec  31737  circlemeth  32616  hgt750lemd  32624  logdivsqrle  32626  subfacp1lem6  33143  subfacval2  33145  subfaclim  33146  cvxsconn  33201  resconn  33204  fwddifnp1  34463  itg2addnclem3  35826  itgmulc2nc  35841  rrnequiv  35989  aks4d1p1p7  40079  fltnlta  40497  cu3addd  40499  3cubeslem2  40504  3cubeslem3r  40506  jm2.19lem3  40810  jm2.25  40818  jm3.1lem2  40837  inductionexd  41735  int-leftdistd  41760  binomcxplemwb  41936  binomcxplemnotnn0  41944  sineq0ALT  42527  fperiodmullem  42813  xralrple2  42864  coskpi2  43378  cosknegpi  43381  dvnmul  43455  stoweidlem11  43523  stoweidlem13  43525  stirlinglem1  43586  stirlinglem4  43589  dirkerper  43608  dirkertrigeqlem1  43610  dirkertrigeqlem2  43611  dirkertrigeqlem3  43612  dirkercncflem2  43616  fourierdlem41  43660  fourierdlem42  43661  fourierdlem64  43682  fourierswlem  43742  hoidmvlelem2  44105  sigaraf  44337  fmtnorec3  44969  itscnhlc0yqe  46074  itsclc0yqsollem1  46077  itscnhlc0xyqsol  46080  itsclc0xyqsolr  46084  itsclquadb  46091  2itscplem3  46095  itscnhlinecirc02plem1  46097