Theorem adddid 10983

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858   · cmul 10860

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  addid1  11138  cnegex  11139  addcom  11144  addcomd  11160  subdi  11391  conjmul  11675  cju  11952  flhalf  13531  modcyc  13607  addmodlteq  13647  binom3  13920  sqoddm1div8  13939  bcpasc  14016  hashf1lem2  14151  remim  14809  mulre  14813  readd  14818  remullem  14820  imadd  14826  cjadd  14833  sqreulem  15052  iseraltlem2  15375  o1fsum  15506  binomlem  15522  climcndslem2  15543  binomfallfaclem2  15731  bpoly4  15750  tanval3  15824  sinadd  15854  tanadd  15857  dvdsmulgcd  16246  lcmgcdlem  16292  pythagtriplem1  16498  pcaddlem  16570  prmreclem4  16601  prmreclem6  16603  mul4sqlem  16635  vdwlem3  16665  vdwlem6  16668  vdwlem9  16671  nn0srg  20649  rge0srg  20650  mhppwdeg  21321  icopnfcnv  24086  pcoass  24168  cphipval2  24386  minveclem2  24571  pjthlem1  24582  ovolunlem1a  24641  ovolscalem1  24658  itgcnlem  24935  itgadd  24970  itgmulc2  24979  itgsplit  24981  aaliou3lem2  25484  abelthlem7  25578  tangtx  25643  efgh  25678  tanarg  25755  logcnlem4  25781  mulcxp  25821  cxpmul2  25825  heron  25969  quad2  25970  dcubic1lem  25974  dcubic2  25975  mcubic  25978  binom4  25981  quart1  25987  atanlogsublem  26046  2efiatan  26049  lgamgulmlem3  26161  basellem2  26212  basellem3  26213  basellem8  26218  chtub  26341  bposlem9  26421  lgseisenlem2  26505  2lgsoddprmlem2  26538  2sqlem4  26550  2sqlem8  26555  dchrisumlem1  26618  dchrvmasum2if  26626  dchrisum0re  26642  mulog2sumlem1  26663  selberglem1  26674  selberglem2  26675  selberg  26677  selberg2  26680  chpdifbndlem1  26682  selberg3lem1  26686  selberg4  26690  pntsval2  26705  pntibndlem2  26720  pntlemr  26731  pntlemf  26734  pntlemo  26736  ostth2lem2  26763  ostth2lem3  26764  brbtwn2  27254  axsegconlem9  27274  axpasch  27290  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  axcontlem8  27320  finsumvtxdg2ssteplem4  27896  ipasslem2  29173  minvecolem2  29216  pjhthlem1  29732  wrdt2ind  31204  ccfldsrarelvec  31720  circlemeth  32599  subfacval2  33128  subfaclim  33129  faclimlem1  33688  itgaddnc  35816  itgmulc2nc  35824  dvasin  35840  2np3bcnp1  40080  nnadddir  40280  nnmul1com  40281  nnmulcom  40282  resubdi  40359  sn-negex12  40378  sn-mul01  40387  sn-mulid2  40397  sn-0tie0  40401  sn-mul02  40402  cnreeu  40418  fltmul  40452  cu3addd  40482  3cubeslem3l  40488  3cubeslem3r  40489  pellexlem6  40636  pell1234qrmulcl  40657  rmxyadd  40723  jm2.25  40801  relexpmulnn  41270  binomcxplemnotnn0  41927  sumnnodd  43125  dvnmul  43438  stoweidlem13  43508  wallispilem4  43563  wallispi2lem1  43566  wallispi2lem2  43567  stirlinglem1  43569  stirlinglem6  43574  stirlinglem7  43575  stirlinglem8  43576  stirlinglem10  43578  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  fourierdlem83  43684  hoidmvlelem2  44088  hspmbllem1  44118  smfmullem1  44276  deccarry  44755  fmtnorec4  44953  mod42tp1mod8  45006  lighneallem3  45011  opoeALTV  45087  opeoALTV  45088  2zlidl  45444  2zrngamgm  45449  altgsumbcALT  45641  itcovalpclem2  45969  ackval2  45980  affinecomb2  46001  itscnhlc0yqe  46057  itsclc0yqsollem1  46060  itsclc0yqsol  46062  itscnhlc0xyqsol  46063  itsclc0xyqsolr  46067  itscnhlinecirc02plem1  46080