Theorem adddird 11286

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158   · cmul 11160

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 2708  ax-addcl 11215  ax-mulcom 11219  ax-distr 11222

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  adddirp1d  11287  joinlmuladdmuld  11288  addmulsub  11725  recextlem1  11893  divdir  11947  subsq  14249  subsq2  14250  binom3  14263  discr1  14278  cshweqrep  14859  remullem  15167  01sqrexlem7  15287  binomlem  15865  binomfallfaclem2  16076  pwp1fsum  16428  smumullem  16529  mul4sqlem  16991  vdwapun  17012  nn0srg  21455  rge0srg  21456  nmotri  24760  blcvx  24819  cphipval2  25275  itg1addlem5  25735  itgconst  25854  dvexp  25991  dvcvx  26059  plyaddlem1  26252  abelthlem7  26482  cxpadd  26721  dcubic  26889  binom4  26893  dquartlem2  26895  dquart  26896  quart1lem  26898  quart1  26899  cvxcl  27028  scvxcvx  27029  basellem9  27132  bposlem9  27336  lgsquad2lem1  27428  2sqlem4  27465  2sqblem  27475  dchrisumlem2  27534  dchrisum0lem1  27560  mudivsum  27574  chpdifbndlem1  27597  pntrlog2bndlem2  27622  pntlemr  27646  pntlemk  27650  ostth2lem2  27678  brbtwn2  28920  ax5seglem3  28946  ax5seglem5  28948  axbtwnid  28954  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  ex-ind-dvds  30480  smcnlem  30716  ccfldsrarelvec  33721  constrrtll  33772  constrrtcclem  33775  constrrtcc  33776  circlemeth  34655  hgt750lemd  34663  logdivsqrle  34665  subfacp1lem6  35190  subfacval2  35192  subfaclim  35193  cvxsconn  35248  resconn  35251  fwddifnp1  36166  itg2addnclem3  37680  itgmulc2nc  37695  rrnequiv  37842  aks4d1p1p7  42075  primrootscoprmpow  42100  fltnlta  42673  cu3addd  42691  3cubeslem2  42696  3cubeslem3r  42698  jm2.19lem3  43003  jm2.25  43011  jm3.1lem2  43030  inductionexd  44168  int-leftdistd  44192  binomcxplemwb  44367  binomcxplemnotnn0  44375  sineq0ALT  44957  fperiodmullem  45315  xralrple2  45365  coskpi2  45881  cosknegpi  45884  dvnmul  45958  stoweidlem11  46026  stoweidlem13  46028  stirlinglem1  46089  stirlinglem4  46092  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem2  46119  fourierdlem41  46163  fourierdlem42  46164  fourierdlem64  46185  fourierswlem  46245  hoidmvlelem2  46611  sigaraf  46868  fmtnorec3  47535  itscnhlc0yqe  48680  itsclc0yqsollem1  48683  itscnhlc0xyqsol  48686  itsclc0xyqsolr  48690  itsclquadb  48697  2itscplem3  48701  itscnhlinecirc02plem1  48703