Theorem adddid 11238

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113   · cmul 11115

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090

This theorem is referenced by:  addrid  11394  cnegex  11395  addcom  11400  addcomd  11416  subdi  11647  conjmul  11931  cju  12208  flhalf  13795  modcyc  13871  addmodlteq  13911  binom3  14187  sqoddm1div8  14206  bcpasc  14281  hashf1lem2  14417  remim  15064  mulre  15068  readd  15073  remullem  15075  imadd  15081  cjadd  15088  sqreulem  15306  iseraltlem2  15629  o1fsum  15759  binomlem  15775  climcndslem2  15796  binomfallfaclem2  15984  bpoly4  16003  tanval3  16077  sinadd  16107  tanadd  16110  dvdsmulgcd  16497  lcmgcdlem  16543  pythagtriplem1  16749  pcaddlem  16821  prmreclem4  16852  prmreclem6  16854  mul4sqlem  16886  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  nn0srg  21015  rge0srg  21016  mhppwdeg  21693  icopnfcnv  24458  pcoass  24540  cphipval2  24758  minveclem2  24943  pjthlem1  24954  ovolunlem1a  25013  ovolscalem1  25030  itgcnlem  25307  itgadd  25342  itgmulc2  25351  itgsplit  25353  aaliou3lem2  25856  abelthlem7  25950  tangtx  26015  efgh  26050  tanarg  26127  logcnlem4  26153  mulcxp  26193  cxpmul2  26197  heron  26343  quad2  26344  dcubic1lem  26348  dcubic2  26349  mcubic  26352  binom4  26355  quart1  26361  atanlogsublem  26420  2efiatan  26423  lgamgulmlem3  26535  basellem2  26586  basellem3  26587  basellem8  26592  chtub  26715  bposlem9  26795  lgseisenlem2  26879  2lgsoddprmlem2  26912  2sqlem4  26924  2sqlem8  26929  dchrisumlem1  26992  dchrvmasum2if  27000  dchrisum0re  27016  mulog2sumlem1  27037  selberglem1  27048  selberglem2  27049  selberg  27051  selberg2  27054  chpdifbndlem1  27056  selberg3lem1  27060  selberg4  27064  pntsval2  27079  pntibndlem2  27094  pntlemr  27105  pntlemf  27108  pntlemo  27110  ostth2lem2  27137  ostth2lem3  27138  brbtwn2  28163  axsegconlem9  28183  axpasch  28199  axeuclidlem  28220  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  finsumvtxdg2ssteplem4  28805  ipasslem2  30085  minvecolem2  30128  pjhthlem1  30644  wrdt2ind  32117  ccfldsrarelvec  32745  circlemeth  33652  subfacval2  34178  subfaclim  34179  faclimlem1  34713  itgaddnc  36548  itgmulc2nc  36556  dvasin  36572  2np3bcnp1  40960  nnadddir  41184  nnmul1com  41185  nnmulcom  41186  sumcubes  41211  resubdi  41269  sn-negex12  41289  sn-mul01  41298  sn-mullid  41308  sn-0tie0  41312  sn-mul02  41313  renegmulnnass  41326  cnreeu  41341  fltmul  41377  cu3addd  41418  3cubeslem3l  41424  3cubeslem3r  41425  pellexlem6  41572  pell1234qrmulcl  41593  rmxyadd  41660  jm2.25  41738  relexpmulnn  42460  binomcxplemnotnn0  43115  sumnnodd  44346  dvnmul  44659  stoweidlem13  44729  wallispilem4  44784  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem1  44790  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  fourierdlem83  44905  hoidmvlelem2  45312  hspmbllem1  45342  smfmullem1  45507  deccarry  46019  fmtnorec4  46217  mod42tp1mod8  46270  lighneallem3  46275  opoeALTV  46351  opeoALTV  46352  2zlidl  46832  2zrngamgm  46837  altgsumbcALT  47029  itcovalpclem2  47357  ackval2  47368  affinecomb2  47389  itscnhlc0yqe  47445  itsclc0yqsollem1  47448  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itsclc0xyqsolr  47455  itscnhlinecirc02plem1  47468