Theorem adddird 11283

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-addcl 11212  ax-mulcom 11216  ax-distr 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  adddirp1d  11284  joinlmuladdmuld  11285  addmulsub  11722  recextlem1  11890  divdir  11944  subsq  14245  subsq2  14246  binom3  14259  discr1  14274  cshweqrep  14855  remullem  15163  01sqrexlem7  15283  binomlem  15861  binomfallfaclem2  16072  pwp1fsum  16424  smumullem  16525  mul4sqlem  16986  vdwapun  17007  nn0srg  21472  rge0srg  21473  nmotri  24775  blcvx  24833  cphipval2  25288  itg1addlem5  25749  itgconst  25868  dvexp  26005  dvcvx  26073  plyaddlem1  26266  abelthlem7  26496  cxpadd  26735  dcubic  26903  binom4  26907  dquartlem2  26909  dquart  26910  quart1lem  26912  quart1  26913  cvxcl  27042  scvxcvx  27043  basellem9  27146  bposlem9  27350  lgsquad2lem1  27442  2sqlem4  27479  2sqblem  27489  dchrisumlem2  27548  dchrisum0lem1  27574  mudivsum  27588  chpdifbndlem1  27611  pntrlog2bndlem2  27636  pntlemr  27660  pntlemk  27664  ostth2lem2  27692  brbtwn2  28934  ax5seglem3  28960  ax5seglem5  28962  axbtwnid  28968  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  ex-ind-dvds  30489  smcnlem  30725  ccfldsrarelvec  33695  constrrtll  33736  constrrtcclem  33739  constrrtcc  33740  circlemeth  34633  hgt750lemd  34641  logdivsqrle  34643  subfacp1lem6  35169  subfacval2  35171  subfaclim  35172  cvxsconn  35227  resconn  35230  fwddifnp1  36146  itg2addnclem3  37659  itgmulc2nc  37674  rrnequiv  37821  aks4d1p1p7  42055  primrootscoprmpow  42080  fltnlta  42649  cu3addd  42667  3cubeslem2  42672  3cubeslem3r  42674  jm2.19lem3  42979  jm2.25  42987  jm3.1lem2  43006  inductionexd  44144  int-leftdistd  44168  binomcxplemwb  44343  binomcxplemnotnn0  44351  sineq0ALT  44934  fperiodmullem  45253  xralrple2  45303  coskpi2  45821  cosknegpi  45824  dvnmul  45898  stoweidlem11  45966  stoweidlem13  45968  stirlinglem1  46029  stirlinglem4  46032  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem2  46059  fourierdlem41  46103  fourierdlem42  46104  fourierdlem64  46125  fourierswlem  46185  hoidmvlelem2  46551  sigaraf  46808  fmtnorec3  47472  itscnhlc0yqe  48608  itsclc0yqsollem1  48611  itscnhlc0xyqsol  48614  itsclc0xyqsolr  48618  itsclquadb  48625  2itscplem3  48629  itscnhlinecirc02plem1  48631