Theorem adddird 11260

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   + caddc 11132   · cmul 11134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-addcl 11189  ax-mulcom 11193  ax-distr 11196

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  adddirp1d  11261  joinlmuladdmuld  11262  addmulsub  11699  recextlem1  11867  divdir  11921  subsq  14228  subsq2  14229  binom3  14242  discr1  14257  cshweqrep  14839  remullem  15147  01sqrexlem7  15267  binomlem  15845  binomfallfaclem2  16056  pwp1fsum  16410  smumullem  16511  mul4sqlem  16973  vdwapun  16994  nn0srg  21405  rge0srg  21406  nmotri  24678  blcvx  24737  cphipval2  25193  itg1addlem5  25653  itgconst  25772  dvexp  25909  dvcvx  25977  plyaddlem1  26170  abelthlem7  26400  cxpadd  26640  dcubic  26808  binom4  26812  dquartlem2  26814  dquart  26815  quart1lem  26817  quart1  26818  cvxcl  26947  scvxcvx  26948  basellem9  27051  bposlem9  27255  lgsquad2lem1  27347  2sqlem4  27384  2sqblem  27394  dchrisumlem2  27453  dchrisum0lem1  27479  mudivsum  27493  chpdifbndlem1  27516  pntrlog2bndlem2  27541  pntlemr  27565  pntlemk  27569  ostth2lem2  27597  brbtwn2  28884  ax5seglem3  28910  ax5seglem5  28912  axbtwnid  28918  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  ex-ind-dvds  30442  smcnlem  30678  ccfldsrarelvec  33712  constrrtll  33765  constrrtcclem  33768  constrrtcc  33769  cos9thpiminplylem2  33817  circlemeth  34672  hgt750lemd  34680  logdivsqrle  34682  subfacp1lem6  35207  subfacval2  35209  subfaclim  35210  cvxsconn  35265  resconn  35268  fwddifnp1  36183  itg2addnclem3  37697  itgmulc2nc  37712  rrnequiv  37859  aks4d1p1p7  42087  primrootscoprmpow  42112  fltnlta  42686  cu3addd  42704  3cubeslem2  42708  3cubeslem3r  42710  jm2.19lem3  43015  jm2.25  43023  jm3.1lem2  43042  inductionexd  44179  int-leftdistd  44203  binomcxplemwb  44372  binomcxplemnotnn0  44380  sineq0ALT  44961  fperiodmullem  45332  xralrple2  45381  coskpi2  45895  cosknegpi  45898  dvnmul  45972  stoweidlem11  46040  stoweidlem13  46042  stirlinglem1  46103  stirlinglem4  46106  dirkerper  46125  dirkertrigeqlem1  46127  dirkertrigeqlem2  46128  dirkertrigeqlem3  46129  dirkercncflem2  46133  fourierdlem41  46177  fourierdlem42  46178  fourierdlem64  46199  fourierswlem  46259  hoidmvlelem2  46625  sigaraf  46882  fmtnorec3  47562  itscnhlc0yqe  48739  itsclc0yqsollem1  48742  itscnhlc0xyqsol  48745  itsclc0xyqsolr  48749  itsclquadb  48756  2itscplem3  48760  itscnhlinecirc02plem1  48762