Theorem adddird 11238

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11102   + caddc 11107   · cmul 11109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-addcl 11164  ax-mulcom 11168  ax-distr 11171

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  adddirp1d  11239  joinlmuladdmuld  11240  addmulsub  11680  recextlem1  11848  divdir  11901  subsq  14251  subsq2  14252  binom3  14265  discr1  14280  cshweqrep  14863  remullem  15184  01sqrexlem7  15304  binomlem  15888  binomfallfaclem2  16098  pwp1fsum  16453  smumullem  16554  mul4sqlem  17017  vdwapun  17038  nn0srg  21596  rge0srg  21597  nmotri  24905  blcvx  24964  cphipval2  25409  itg1addlem5  25868  itgconst  25987  dvexp  26121  dvcvx  26188  plyaddlem1  26379  abelthlem7  26610  cxpadd  26853  dcubic  27020  binom4  27024  dquartlem2  27026  dquart  27027  quart1lem  27029  quart1  27030  cvxcl  27158  scvxcvx  27159  basellem9  27262  bposlem9  27465  lgsquad2lem1  27557  2sqlem4  27594  2sqblem  27604  dchrisumlem2  27663  dchrisum0lem1  27689  mudivsum  27703  chpdifbndlem1  27726  pntrlog2bndlem2  27751  pntlemr  27775  pntlemk  27779  ostth2lem2  27807  brbtwn2  29264  ax5seglem3  29290  ax5seglem5  29292  axbtwnid  29298  axeuclidlem  29321  axcontlem2  29324  axcontlem4  29326  axcontlem7  29329  ex-ind-dvds  30821  smcnlem  31058  ccfldsrarelvec  34070  constrrtll  34130  constrrtcclem  34133  constrrtcc  34134  cos9thpiminplylem2  34182  circlemeth  35036  hgt750lemd  35044  logdivsqrle  35046  subfacp1lem6  35685  subfacval2  35687  subfaclim  35688  cvxsconn  35743  resconn  35746  fwddifnp1  36665  itg2addnclem3  38352  itgmulc2nc  38367  rrnequiv  38514  aks4d1p1p7  42869  primrootscoprmpow  42894  3rdpwhole  43081  fltnlta  43423  cu3addd  43440  3cubeslem2  43444  3cubeslem3r  43446  jm2.19lem3  43746  jm2.25  43754  jm3.1lem2  43773  inductionexd  44909  int-leftdistd  44933  binomcxplemwb  45086  binomcxplemnotnn0  45094  sineq0ALT  45673  fperiodmullem  46050  xralrple2  46098  coskpi2  46608  cosknegpi  46611  dvnmul  46685  stoweidlem11  46753  stoweidlem13  46755  stirlinglem1  46816  stirlinglem4  46819  dirkerper  46838  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkercncflem2  46846  fourierdlem41  46890  fourierdlem42  46891  fourierdlem64  46912  fourierswlem  46972  hoidmvlelem2  47338  sigaraf  47595  sin3t  47636  cos3t  47637  sin5tlem1  47638  sin5tlem5  47642  sin5t  47643  cos5t  47644  fmtnorec3  48328  itscnhlc0yqe  49567  itsclc0yqsollem1  49570  itscnhlc0xyqsol  49573  itsclc0xyqsolr  49577  itsclquadb  49584  2itscplem3  49588  itscnhlinecirc02plem1  49590  crossp3i  50676