Theorem adddird 11373

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242   · cmul 11244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-addcl 11299  ax-mulcom 11303  ax-distr 11306

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  adddirp1d  11374  joinlmuladdmuld  11375  addmulsub  11818  recextlem1  11986  divdir  12039  subsq  14394  subsq2  14395  addmuldir2d  14396  binom3  14409  discr1  14424  cshweqrep  15014  remullem  15338  01sqrexlem7  15458  binomlem  16042  binomfallfaclem2  16250  pwp1fsum  16605  smumullem  16706  mul4sqlem  17175  vdwapun  17196  nn0srg  21797  rge0srg  21798  nmotri  25113  blcvx  25172  cphipval2  25617  itg1addlem5  26076  itgconst  26194  dvexp  26328  dvcvx  26395  plyaddlem1  26587  abelthlem7  26822  cxpadd  27064  dcubic  27231  binom4  27235  dquartlem2  27237  dquart  27238  quart1lem  27240  quart1  27241  cvxcl  27369  scvxcvx  27370  basellem9  27473  bposlem9  27676  lgsquad2lem1  27768  2sqlem4  27805  2sqblem  27815  dchrisumlem2  27874  dchrisum0lem1  27900  mudivsum  27914  chpdifbndlem1  27937  pntrlog2bndlem2  27962  pntlemr  27986  pntlemk  27990  ostth2lem2  28018  brbtwn2  29540  ax5seglem3  29566  ax5seglem5  29568  axbtwnid  29574  axeuclidlem  29597  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  ex-ind-dvds  31119  smcnlem  31356  ccfldsrarelvec  34414  constrrtll  34474  constrrtcclem  34477  constrrtcc  34478  cos9thpiminplylem2  34526  circlemeth  35380  hgt750lemd  35388  logdivsqrle  35390  subfacp1lem6  36158  subfacval2  36160  subfaclim  36161  cvxsconn  36216  resconn  36219  fwddifnp1  37145  itg2addnclem3  38859  itgmulc2nc  38874  rrnequiv  39035  aks4d1p1p7  43390  primrootscoprmpow  43415  3rdpwhole  43615  fltnlta  43940  cu3addd  43957  3cubeslem2  43961  3cubeslem3r  43963  jm2.19lem3  44264  jm2.25  44272  jm3.1lem2  44291  inductionexd  45416  int-leftdistd  45440  binomcxplemwb  45593  binomcxplemnotnn0  45601  sineq0ALT  46179  fperiodmullem  46592  xralrple2  46639  coskpi2  47149  cosknegpi  47152  dvnmul  47226  stoweidlem11  47294  stoweidlem13  47296  stirlinglem1  47357  stirlinglem4  47360  dirkerper  47379  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkercncflem2  47387  fourierdlem41  47431  fourierdlem42  47432  fourierdlem64  47453  fourierswlem  47513  hoidmvlelem2  47879  sigaraf  48136  sin3t  48190  cos3t  48191  sin5tlem1  48192  sin5tlem5  48196  sin5t  48197  cos5t  48198  fmtnorec3  48906  lazaddcl  49738  itscnhlc0yqe  50202  itsclc0yqsollem1  50205  itscnhlc0xyqsol  50208  itsclc0xyqsolr  50212  itsclquadb  50219  2itscplem3  50223  itscnhlinecirc02plem1  50225  crossp3d  51395