Theorem adddird 11327

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191   + caddc 11196   · cmul 11198

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-addcl 11253  ax-mulcom 11257  ax-distr 11260

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421

This theorem is used by:  adddirp1d  11328  joinlmuladdmuld  11329  addmulsub  11771  recextlem1  11939  divdir  11992  subsq  14347  subsq2  14348  binom3  14361  discr1  14376  cshweqrep  14965  remullem  15288  01sqrexlem7  15408  binomlem  15991  binomfallfaclem2  16199  pwp1fsum  16554  smumullem  16655  mul4sqlem  17124  vdwapun  17145  nn0srg  21736  rge0srg  21737  nmotri  25051  blcvx  25110  cphipval2  25555  itg1addlem5  26014  itgconst  26132  dvexp  26266  dvcvx  26333  plyaddlem1  26525  abelthlem7  26758  cxpadd  27000  dcubic  27167  binom4  27171  dquartlem2  27173  dquart  27174  quart1lem  27176  quart1  27177  cvxcl  27305  scvxcvx  27306  basellem9  27409  bposlem9  27612  lgsquad2lem1  27704  2sqlem4  27741  2sqblem  27751  dchrisumlem2  27810  dchrisum0lem1  27836  mudivsum  27850  chpdifbndlem1  27873  pntrlog2bndlem2  27898  pntlemr  27922  pntlemk  27926  ostth2lem2  27954  brbtwn2  29476  ax5seglem3  29502  ax5seglem5  29504  axbtwnid  29510  axeuclidlem  29533  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  ex-ind-dvds  31055  smcnlem  31292  ccfldsrarelvec  34296  constrrtll  34356  constrrtcclem  34359  constrrtcc  34360  cos9thpiminplylem2  34408  circlemeth  35262  hgt750lemd  35270  logdivsqrle  35272  subfacp1lem6  35929  subfacval2  35931  subfaclim  35932  cvxsconn  35987  resconn  35990  fwddifnp1  36910  itg2addnclem3  38571  itgmulc2nc  38586  rrnequiv  38749  aks4d1p1p7  43104  primrootscoprmpow  43129  3rdpwhole  43329  fltnlta  43654  cu3addd  43671  3cubeslem2  43675  3cubeslem3r  43677  jm2.19lem3  43977  jm2.25  43985  jm3.1lem2  44004  inductionexd  45140  int-leftdistd  45164  binomcxplemwb  45317  binomcxplemnotnn0  45325  sineq0ALT  45904  fperiodmullem  46288  xralrple2  46335  coskpi2  46845  cosknegpi  46848  dvnmul  46922  stoweidlem11  46990  stoweidlem13  46992  stirlinglem1  47053  stirlinglem4  47056  dirkerper  47075  dirkertrigeqlem1  47077  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkercncflem2  47083  fourierdlem41  47127  fourierdlem42  47128  fourierdlem64  47149  fourierswlem  47209  hoidmvlelem2  47575  sigaraf  47832  sin3t  47886  cos3t  47887  sin5tlem1  47888  sin5tlem5  47892  sin5t  47893  cos5t  47894  fmtnorec3  48602  itscnhlc0yqe  49840  itsclc0yqsollem1  49843  itscnhlc0xyqsol  49846  itsclc0xyqsolr  49850  itsclquadb  49857  2itscplem3  49861  itscnhlinecirc02plem1  49863  crossp3d  50936