Theorem adddird 10389

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

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164  (class class class)co 6910  ℂcc 10257   + caddc 10262   · cmul 10264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-addcl 10319  ax-mulcom 10323  ax-distr 10326

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913

This theorem is referenced by:  adddirp1d  10390  joinlmuladdmuld  10391  recextlem1  10989  divdir  11042  ltdifltdiv  12937  subsq  13273  subsq2  13274  binom3  13286  discr1  13301  cshweqrep  13949  remullem  14252  sqrlem7  14373  binomlem  14942  binomfallfaclem2  15150  pwp1fsum  15495  smumullem  15594  bezoutlem3  15638  bezoutlem4  15639  pcexp  15942  mul4sqlem  16035  vdwapun  16056  mulgnnass  17935  cnfldmulg  20145  nn0srg  20183  rge0srg  20184  nmotri  22920  blcvx  22978  cphipval2  23416  itg1addlem5  23873  mbfi1fseqlem4  23891  itgconst  23991  itgmulc2  24006  dvexp  24122  dvcvx  24189  plyaddlem1  24375  dgrcolem1  24435  abelthlem2  24592  abelthlem7  24598  tangtx  24664  cxpadd  24831  dcubic  24993  binom4  24997  dquartlem2  24999  dquart  25000  quart1lem  25002  quart1  25003  cvxcl  25131  scvxcvx  25132  basellem9  25235  bposlem9  25437  lgsquad2lem1  25529  2sqlem4  25566  2sqblem  25576  dchrisumlem2  25599  dchrisum0lem1  25625  mudivsum  25639  chpdifbndlem1  25662  pntrlog2bndlem2  25687  pntlemr  25711  pntlemk  25715  ostth2lem2  25743  brbtwn2  26211  ax5seglem3  26237  ax5seglem5  26239  axbtwnid  26245  axeuclidlem  26268  axcontlem2  26271  axcontlem4  26273  axcontlem7  26276  axcontlem8  26277  ex-ind-dvds  27872  smcnlem  28103  circlemeth  31263  hgt750lemd  31271  logdivsqrle  31273  subfacp1lem6  31709  subfacval2  31711  subfaclim  31712  cvxsconn  31767  resconn  31770  fwddifnp1  32806  itg2addnclem3  34001  itgmulc2nc  34016  rrnequiv  34171  jm2.19lem3  38396  jm2.25  38404  jm3.1lem2  38423  inductionexd  39288  int-leftdistd  39317  binomcxplemwb  39382  binomcxplemnotnn0  39390  sineq0ALT  39986  fperiodmullem  40309  xralrple2  40361  coskpi2  40866  cosknegpi  40869  dvnmul  40947  stoweidlem11  41016  stoweidlem13  41018  stirlinglem1  41079  stirlinglem4  41082  dirkerper  41101  dirkertrigeqlem1  41103  dirkertrigeqlem2  41104  dirkertrigeqlem3  41105  dirkercncflem2  41109  fourierdlem41  41153  fourierdlem42  41154  fourierdlem64  41175  fourierswlem  41235  hoidmvlelem2  41598  sigaraf  41830  fmtnorec3  42304  itsclc0lem1  43318  itsclc0lem2  43319  itsclc0lem5  43322