Theorem adddid 11158

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   · cmul 11033

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11314  cnegex  11315  addcom  11320  addcomd  11336  subdi  11571  conjmul  11859  cju  12142  flhalf  13752  modcyc  13828  addmodlteq  13871  binom3  14149  sqoddm1div8  14168  bcpasc  14246  hashf1lem2  14381  remim  15042  mulre  15046  readd  15051  remullem  15053  imadd  15059  cjadd  15066  sqreulem  15285  iseraltlem2  15608  o1fsum  15738  binomlem  15754  climcndslem2  15775  binomfallfaclem2  15965  bpoly4  15984  tanval3  16061  sinadd  16091  tanadd  16094  dvdsmulgcd  16485  lcmgcdlem  16535  pythagtriplem1  16746  pcaddlem  16818  prmreclem4  16849  prmreclem6  16851  mul4sqlem  16883  vdwlem3  16913  vdwlem6  16916  vdwlem9  16919  nn0srg  21362  rge0srg  21363  mhppwdeg  22053  icopnfcnv  24856  pcoass  24940  cphipval2  25157  minveclem2  25342  pjthlem1  25353  ovolunlem1a  25413  ovolscalem1  25430  itgcnlem  25707  itgadd  25742  itgmulc2  25751  itgsplit  25753  aaliou3lem2  26267  abelthlem7  26364  tangtx  26430  efgh  26466  tanarg  26544  logcnlem4  26570  mulcxp  26610  cxpmul2  26614  heron  26764  quad2  26765  dcubic1lem  26769  dcubic2  26770  mcubic  26773  binom4  26776  quart1  26782  atanlogsublem  26841  2efiatan  26844  lgamgulmlem3  26957  basellem2  27008  basellem3  27009  basellem8  27014  chtub  27139  bposlem9  27219  lgseisenlem2  27303  2lgsoddprmlem2  27336  2sqlem4  27348  2sqlem8  27353  dchrisumlem1  27416  dchrvmasum2if  27424  dchrisum0re  27440  mulog2sumlem1  27461  selberglem1  27472  selberglem2  27473  selberg  27475  selberg2  27478  chpdifbndlem1  27480  selberg3lem1  27484  selberg4  27488  pntsval2  27503  pntibndlem2  27518  pntlemr  27529  pntlemf  27532  pntlemo  27534  ostth2lem2  27561  ostth2lem3  27562  brbtwn2  28868  axsegconlem9  28888  axpasch  28904  axeuclidlem  28925  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  finsumvtxdg2ssteplem4  29512  ipasslem2  30794  minvecolem2  30837  pjhthlem1  31353  wrdt2ind  32908  ccfldsrarelvec  33645  constrrtcclem  33703  constrremulcl  33736  constrrecl  33738  circlemeth  34610  subfacval2  35162  subfaclim  35163  faclimlem1  35718  itgaddnc  37662  itgmulc2nc  37670  dvasin  37686  posbezout  42076  2np3bcnp1  42120  nnadddir  42246  nnmul1com  42247  nnmulcom  42248  sumcubes  42289  resubdi  42372  sn-negex12  42393  sn-mul01  42402  sn-mullid  42412  sn-0tie0  42427  sn-mul02  42428  renegmulnnass  42441  cnreeu  42466  fltmul  42611  cu3addd  42657  3cubeslem3l  42662  3cubeslem3r  42663  pellexlem6  42810  pell1234qrmulcl  42831  rmxyadd  42897  jm2.25  42975  relexpmulnn  43685  binomcxplemnotnn0  44332  sumnnodd  45615  dvnmul  45928  stoweidlem13  45998  wallispilem4  46053  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem1  46059  stirlinglem6  46064  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  dirkerper  46081  dirkertrigeqlem1  46083  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  fourierdlem83  46174  hoidmvlelem2  46581  hspmbllem1  46611  smfmullem1  46776  deccarry  47299  fmtnorec4  47537  mod42tp1mod8  47590  lighneallem3  47595  opoeALTV  47671  opeoALTV  47672  2zlidl  48228  2zrngamgm  48233  altgsumbcALT  48341  itcovalpclem2  48660  ackval2  48671  affinecomb2  48692  itscnhlc0yqe  48748  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itscnhlinecirc02plem1  48771