Theorem adddird 11170

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-addcl 11098  ax-mulcom 11102  ax-distr 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  adddirp1d  11171  joinlmuladdmuld  11172  addmulsub  11612  recextlem1  11780  divdir  11834  subsq  14172  subsq2  14173  binom3  14186  discr1  14201  cshweqrep  14783  remullem  15090  01sqrexlem7  15210  binomlem  15794  binomfallfaclem2  16005  pwp1fsum  16360  smumullem  16461  mul4sqlem  16924  vdwapun  16945  nn0srg  21417  rge0srg  21418  nmotri  24704  blcvx  24763  cphipval2  25208  itg1addlem5  25667  itgconst  25786  dvexp  25920  dvcvx  25987  plyaddlem1  26178  abelthlem7  26403  cxpadd  26643  dcubic  26810  binom4  26814  dquartlem2  26816  dquart  26817  quart1lem  26819  quart1  26820  cvxcl  26948  scvxcvx  26949  basellem9  27052  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  28974  ax5seglem3  29000  ax5seglem5  29002  axbtwnid  29008  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  ex-ind-dvds  30531  smcnlem  30768  ccfldsrarelvec  33815  constrrtll  33875  constrrtcclem  33878  constrrtcc  33879  cos9thpiminplylem2  33927  circlemeth  34784  hgt750lemd  34792  logdivsqrle  34794  subfacp1lem6  35367  subfacval2  35369  subfaclim  35370  cvxsconn  35425  resconn  35428  fwddifnp1  36347  itg2addnclem3  37994  itgmulc2nc  38009  rrnequiv  38156  aks4d1p1p7  42513  primrootscoprmpow  42538  3rdpwhole  42724  fltnlta  43096  cu3addd  43113  3cubeslem2  43117  3cubeslem3r  43119  jm2.19lem3  43419  jm2.25  43427  jm3.1lem2  43446  inductionexd  44582  int-leftdistd  44606  binomcxplemwb  44775  binomcxplemnotnn0  44783  sineq0ALT  45363  fperiodmullem  45736  xralrple2  45784  coskpi2  46294  cosknegpi  46297  dvnmul  46371  stoweidlem11  46439  stoweidlem13  46441  stirlinglem1  46502  stirlinglem4  46505  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem2  46532  fourierdlem41  46576  fourierdlem42  46577  fourierdlem64  46598  fourierswlem  46658  hoidmvlelem2  47024  sigaraf  47281  sin3t  47319  cos3t  47320  sin5tlem1  47321  sin5tlem5  47325  sin5t  47326  cos5t  47327  fmtnorec3  48011  itscnhlc0yqe  49235  itsclc0yqsollem1  49238  itscnhlc0xyqsol  49241  itsclc0xyqsolr  49245  itsclquadb  49252  2itscplem3  49256  itscnhlinecirc02plem1  49258