Theorem adddid 10665

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddid	⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddi 10626	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  addid1  10820  cnegex  10821  addcom  10826  addcomd  10842  subdi  11073  conjmul  11357  cju  11634  flhalf  13201  modcyc  13275  addmodlteq  13315  binom3  13586  sqoddm1div8  13605  bcpasc  13682  hashf1lem2  13815  remim  14476  mulre  14480  readd  14485  remullem  14487  imadd  14493  cjadd  14500  sqreulem  14719  iseraltlem2  15039  o1fsum  15168  binomlem  15184  climcndslem2  15205  binomfallfaclem2  15394  bpoly4  15413  tanval3  15487  sinadd  15517  tanadd  15520  dvdsmulgcd  15905  lcmgcdlem  15950  pythagtriplem1  16153  pcaddlem  16224  prmreclem4  16255  prmreclem6  16257  mul4sqlem  16289  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  nn0srg  20615  rge0srg  20616  icopnfcnv  23546  pcoass  23628  cphipval2  23844  minveclem2  24029  pjthlem1  24040  ovolunlem1a  24097  ovolscalem1  24114  itgcnlem  24390  itgadd  24425  itgmulc2  24434  itgsplit  24436  aaliou3lem2  24932  abelthlem7  25026  tangtx  25091  efgh  25125  tanarg  25202  logcnlem4  25228  mulcxp  25268  cxpmul2  25272  heron  25416  quad2  25417  dcubic1lem  25421  dcubic2  25422  mcubic  25425  binom4  25428  quart1  25434  atanlogsublem  25493  2efiatan  25496  lgamgulmlem3  25608  basellem2  25659  basellem3  25660  basellem8  25665  chtub  25788  bposlem9  25868  lgseisenlem2  25952  2lgsoddprmlem2  25985  2sqlem4  25997  2sqlem8  26002  dchrisumlem1  26065  dchrvmasum2if  26073  dchrisum0re  26089  mulog2sumlem1  26110  selberglem1  26121  selberglem2  26122  selberg  26124  selberg2  26127  chpdifbndlem1  26129  selberg3lem1  26133  selberg4  26137  pntsval2  26152  pntibndlem2  26167  pntlemr  26178  pntlemf  26181  pntlemo  26183  ostth2lem2  26210  ostth2lem3  26211  brbtwn2  26691  axsegconlem9  26711  axpasch  26727  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  finsumvtxdg2ssteplem4  27330  ipasslem2  28609  minvecolem2  28652  pjhthlem1  29168  wrdt2ind  30627  ccfldsrarelvec  31056  circlemeth  31911  subfacval2  32434  subfaclim  32435  faclimlem1  32975  itgaddnc  34967  itgmulc2nc  34975  dvasin  34993  nnadddir  39212  nnmul1com  39213  nnmulcom  39214  resubdi  39275  cu3addd  39326  3cubeslem3l  39332  3cubeslem3r  39333  pellexlem6  39480  pell1234qrmulcl  39501  rmxyadd  39567  jm2.25  39645  relexpmulnn  40103  binomcxplemnotnn0  40737  sumnnodd  41960  dvnmul  42277  stoweidlem13  42347  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem1  42408  stirlinglem6  42413  stirlinglem7  42414  stirlinglem8  42415  stirlinglem10  42417  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  fourierdlem83  42523  hoidmvlelem2  42927  hspmbllem1  42957  smfmullem1  43115  deccarry  43560  fmtnorec4  43760  mod42tp1mod8  43816  lighneallem3  43821  opoeALTV  43897  opeoALTV  43898  2zlidl  44254  2zrngamgm  44259  altgsumbcALT  44450  affinecomb2  44739  itscnhlc0yqe  44795  itsclc0yqsollem1  44798  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itsclc0xyqsolr  44805  itscnhlinecirc02plem1  44818