Theorem adddid 11045

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   + caddc 10920   · cmul 10922

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

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

This theorem is referenced by:  addid1  11201  cnegex  11202  addcom  11207  addcomd  11223  subdi  11454  conjmul  11738  cju  12015  flhalf  13596  modcyc  13672  addmodlteq  13712  binom3  13985  sqoddm1div8  14004  bcpasc  14081  hashf1lem2  14215  remim  14873  mulre  14877  readd  14882  remullem  14884  imadd  14890  cjadd  14897  sqreulem  15116  iseraltlem2  15439  o1fsum  15570  binomlem  15586  climcndslem2  15607  binomfallfaclem2  15795  bpoly4  15814  tanval3  15888  sinadd  15918  tanadd  15921  dvdsmulgcd  16310  lcmgcdlem  16356  pythagtriplem1  16562  pcaddlem  16634  prmreclem4  16665  prmreclem6  16667  mul4sqlem  16699  vdwlem3  16729  vdwlem6  16732  vdwlem9  16735  nn0srg  20713  rge0srg  20714  mhppwdeg  21385  icopnfcnv  24150  pcoass  24232  cphipval2  24450  minveclem2  24635  pjthlem1  24646  ovolunlem1a  24705  ovolscalem1  24722  itgcnlem  24999  itgadd  25034  itgmulc2  25043  itgsplit  25045  aaliou3lem2  25548  abelthlem7  25642  tangtx  25707  efgh  25742  tanarg  25819  logcnlem4  25845  mulcxp  25885  cxpmul2  25889  heron  26033  quad2  26034  dcubic1lem  26038  dcubic2  26039  mcubic  26042  binom4  26045  quart1  26051  atanlogsublem  26110  2efiatan  26113  lgamgulmlem3  26225  basellem2  26276  basellem3  26277  basellem8  26282  chtub  26405  bposlem9  26485  lgseisenlem2  26569  2lgsoddprmlem2  26602  2sqlem4  26614  2sqlem8  26619  dchrisumlem1  26682  dchrvmasum2if  26690  dchrisum0re  26706  mulog2sumlem1  26727  selberglem1  26738  selberglem2  26739  selberg  26741  selberg2  26744  chpdifbndlem1  26746  selberg3lem1  26750  selberg4  26754  pntsval2  26769  pntibndlem2  26784  pntlemr  26795  pntlemf  26798  pntlemo  26800  ostth2lem2  26827  ostth2lem3  26828  brbtwn2  27318  axsegconlem9  27338  axpasch  27354  axeuclidlem  27375  axcontlem2  27378  axcontlem4  27380  axcontlem7  27383  axcontlem8  27384  finsumvtxdg2ssteplem4  27960  ipasslem2  29239  minvecolem2  29282  pjhthlem1  29798  wrdt2ind  31270  ccfldsrarelvec  31786  circlemeth  32665  subfacval2  33194  subfaclim  33195  faclimlem1  33754  itgaddnc  35881  itgmulc2nc  35889  dvasin  35905  2np3bcnp1  40142  nnadddir  40337  nnmul1com  40338  nnmulcom  40339  resubdi  40416  sn-negex12  40435  sn-mul01  40444  sn-mulid2  40454  sn-0tie0  40458  sn-mul02  40459  cnreeu  40475  fltmul  40509  cu3addd  40539  3cubeslem3l  40545  3cubeslem3r  40546  pellexlem6  40693  pell1234qrmulcl  40714  rmxyadd  40781  jm2.25  40859  relexpmulnn  41355  binomcxplemnotnn0  42012  sumnnodd  43220  dvnmul  43533  stoweidlem13  43603  wallispilem4  43658  wallispi2lem1  43661  wallispi2lem2  43662  stirlinglem1  43664  stirlinglem6  43669  stirlinglem7  43670  stirlinglem8  43671  stirlinglem10  43673  dirkerper  43686  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkertrigeqlem3  43690  fourierdlem83  43779  hoidmvlelem2  44184  hspmbllem1  44214  smfmullem1  44379  deccarry  44861  fmtnorec4  45059  mod42tp1mod8  45112  lighneallem3  45117  opoeALTV  45193  opeoALTV  45194  2zlidl  45550  2zrngamgm  45555  altgsumbcALT  45747  itcovalpclem2  46075  ackval2  46086  affinecomb2  46107  itscnhlc0yqe  46163  itsclc0yqsollem1  46166  itsclc0yqsol  46168  itscnhlc0xyqsol  46169  itsclc0xyqsolr  46173  itscnhlinecirc02plem1  46186