Theorem adddird 11270

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11137   + caddc 11142   · cmul 11144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-addcl 11199  ax-mulcom 11203  ax-distr 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423

This theorem is referenced by:  adddirp1d  11271  joinlmuladdmuld  11272  addmulsub  11707  recextlem1  11875  divdir  11928  subsq  14206  subsq2  14207  binom3  14219  discr1  14234  cshweqrep  14804  remullem  15108  01sqrexlem7  15228  binomlem  15808  binomfallfaclem2  16017  pwp1fsum  16368  smumullem  16467  mul4sqlem  16922  vdwapun  16943  nn0srg  21370  rge0srg  21371  nmotri  24669  blcvx  24727  cphipval2  25182  itg1addlem5  25643  itgconst  25761  dvexp  25898  dvcvx  25966  plyaddlem1  26160  abelthlem7  26388  cxpadd  26626  dcubic  26791  binom4  26795  dquartlem2  26797  dquart  26798  quart1lem  26800  quart1  26801  cvxcl  26930  scvxcvx  26931  basellem9  27034  bposlem9  27238  lgsquad2lem1  27330  2sqlem4  27367  2sqblem  27377  dchrisumlem2  27436  dchrisum0lem1  27462  mudivsum  27476  chpdifbndlem1  27499  pntrlog2bndlem2  27524  pntlemr  27548  pntlemk  27552  ostth2lem2  27580  brbtwn2  28729  ax5seglem3  28755  ax5seglem5  28757  axbtwnid  28763  axeuclidlem  28786  axcontlem2  28789  axcontlem4  28791  axcontlem7  28794  ex-ind-dvds  30284  smcnlem  30520  ccfldsrarelvec  33359  circlemeth  34272  hgt750lemd  34280  logdivsqrle  34282  subfacp1lem6  34795  subfacval2  34797  subfaclim  34798  cvxsconn  34853  resconn  34856  fwddifnp1  35761  itg2addnclem3  37146  itgmulc2nc  37161  rrnequiv  37308  aks4d1p1p7  41545  primrootscoprmpow  41570  fltnlta  42087  cu3addd  42100  3cubeslem2  42105  3cubeslem3r  42107  jm2.19lem3  42412  jm2.25  42420  jm3.1lem2  42439  inductionexd  43585  int-leftdistd  43609  binomcxplemwb  43785  binomcxplemnotnn0  43793  sineq0ALT  44376  fperiodmullem  44685  xralrple2  44736  coskpi2  45254  cosknegpi  45257  dvnmul  45331  stoweidlem11  45399  stoweidlem13  45401  stirlinglem1  45462  stirlinglem4  45465  dirkerper  45484  dirkertrigeqlem1  45486  dirkertrigeqlem2  45487  dirkertrigeqlem3  45488  dirkercncflem2  45492  fourierdlem41  45536  fourierdlem42  45537  fourierdlem64  45558  fourierswlem  45618  hoidmvlelem2  45984  sigaraf  46241  fmtnorec3  46888  itscnhlc0yqe  47832  itsclc0yqsollem1  47835  itscnhlc0xyqsol  47838  itsclc0xyqsolr  47842  itsclquadb  47849  2itscplem3  47853  itscnhlinecirc02plem1  47855