Theorem adddird 11315

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-addcl 11244  ax-mulcom 11248  ax-distr 11251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  adddirp1d  11316  joinlmuladdmuld  11317  addmulsub  11752  recextlem1  11920  divdir  11974  subsq  14259  subsq2  14260  binom3  14273  discr1  14288  cshweqrep  14869  remullem  15177  01sqrexlem7  15297  binomlem  15877  binomfallfaclem2  16088  pwp1fsum  16439  smumullem  16538  mul4sqlem  17000  vdwapun  17021  nn0srg  21478  rge0srg  21479  nmotri  24781  blcvx  24839  cphipval2  25294  itg1addlem5  25755  itgconst  25874  dvexp  26011  dvcvx  26079  plyaddlem1  26272  abelthlem7  26500  cxpadd  26739  dcubic  26907  binom4  26911  dquartlem2  26913  dquart  26914  quart1lem  26916  quart1  26917  cvxcl  27046  scvxcvx  27047  basellem9  27150  bposlem9  27354  lgsquad2lem1  27446  2sqlem4  27483  2sqblem  27493  dchrisumlem2  27552  dchrisum0lem1  27578  mudivsum  27592  chpdifbndlem1  27615  pntrlog2bndlem2  27640  pntlemr  27664  pntlemk  27668  ostth2lem2  27696  brbtwn2  28938  ax5seglem3  28964  ax5seglem5  28966  axbtwnid  28972  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  ex-ind-dvds  30493  smcnlem  30729  ccfldsrarelvec  33681  constrrtll  33722  constrrtcclem  33725  constrrtcc  33726  circlemeth  34617  hgt750lemd  34625  logdivsqrle  34627  subfacp1lem6  35153  subfacval2  35155  subfaclim  35156  cvxsconn  35211  resconn  35214  fwddifnp1  36129  itg2addnclem3  37633  itgmulc2nc  37648  rrnequiv  37795  aks4d1p1p7  42031  primrootscoprmpow  42056  fltnlta  42618  cu3addd  42636  3cubeslem2  42641  3cubeslem3r  42643  jm2.19lem3  42948  jm2.25  42956  jm3.1lem2  42975  inductionexd  44117  int-leftdistd  44141  binomcxplemwb  44317  binomcxplemnotnn0  44325  sineq0ALT  44908  fperiodmullem  45218  xralrple2  45269  coskpi2  45787  cosknegpi  45790  dvnmul  45864  stoweidlem11  45932  stoweidlem13  45934  stirlinglem1  45995  stirlinglem4  45998  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkercncflem2  46025  fourierdlem41  46069  fourierdlem42  46070  fourierdlem64  46091  fourierswlem  46151  hoidmvlelem2  46517  sigaraf  46774  fmtnorec3  47422  itscnhlc0yqe  48493  itsclc0yqsollem1  48496  itscnhlc0xyqsol  48499  itsclc0xyqsolr  48503  itsclquadb  48510  2itscplem3  48514  itscnhlinecirc02plem1  48516