Theorem adddid 11283

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   + caddc 11156   · cmul 11158

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

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

This theorem is referenced by:  addrid  11439  cnegex  11440  addcom  11445  addcomd  11461  subdi  11694  conjmul  11982  cju  12260  flhalf  13867  modcyc  13943  addmodlteq  13984  binom3  14260  sqoddm1div8  14279  bcpasc  14357  hashf1lem2  14492  remim  15153  mulre  15157  readd  15162  remullem  15164  imadd  15170  cjadd  15177  sqreulem  15395  iseraltlem2  15716  o1fsum  15846  binomlem  15862  climcndslem2  15883  binomfallfaclem2  16073  bpoly4  16092  tanval3  16167  sinadd  16197  tanadd  16200  dvdsmulgcd  16590  lcmgcdlem  16640  pythagtriplem1  16850  pcaddlem  16922  prmreclem4  16953  prmreclem6  16955  mul4sqlem  16987  vdwlem3  17017  vdwlem6  17020  vdwlem9  17023  nn0srg  21473  rge0srg  21474  mhppwdeg  22172  icopnfcnv  24987  pcoass  25071  cphipval2  25289  minveclem2  25474  pjthlem1  25485  ovolunlem1a  25545  ovolscalem1  25562  itgcnlem  25840  itgadd  25875  itgmulc2  25884  itgsplit  25886  aaliou3lem2  26400  abelthlem7  26497  tangtx  26562  efgh  26598  tanarg  26676  logcnlem4  26702  mulcxp  26742  cxpmul2  26746  heron  26896  quad2  26897  dcubic1lem  26901  dcubic2  26902  mcubic  26905  binom4  26908  quart1  26914  atanlogsublem  26973  2efiatan  26976  lgamgulmlem3  27089  basellem2  27140  basellem3  27141  basellem8  27146  chtub  27271  bposlem9  27351  lgseisenlem2  27435  2lgsoddprmlem2  27468  2sqlem4  27480  2sqlem8  27485  dchrisumlem1  27548  dchrvmasum2if  27556  dchrisum0re  27572  mulog2sumlem1  27593  selberglem1  27604  selberglem2  27605  selberg  27607  selberg2  27610  chpdifbndlem1  27612  selberg3lem1  27616  selberg4  27620  pntsval2  27635  pntibndlem2  27650  pntlemr  27661  pntlemf  27664  pntlemo  27666  ostth2lem2  27693  ostth2lem3  27694  brbtwn2  28935  axsegconlem9  28955  axpasch  28971  axeuclidlem  28992  axcontlem2  28995  axcontlem4  28997  axcontlem7  29000  axcontlem8  29001  finsumvtxdg2ssteplem4  29581  ipasslem2  30861  minvecolem2  30904  pjhthlem1  31420  wrdt2ind  32923  ccfldsrarelvec  33696  constrrtcclem  33740  circlemeth  34634  subfacval2  35172  subfaclim  35173  faclimlem1  35723  itgaddnc  37667  itgmulc2nc  37675  dvasin  37691  posbezout  42082  2np3bcnp1  42126  nnadddir  42284  nnmul1com  42285  nnmulcom  42286  sumcubes  42326  resubdi  42403  sn-negex12  42423  sn-mul01  42432  sn-mullid  42442  sn-0tie0  42446  sn-mul02  42447  renegmulnnass  42460  cnreeu  42477  fltmul  42622  cu3addd  42668  3cubeslem3l  42674  3cubeslem3r  42675  pellexlem6  42822  pell1234qrmulcl  42843  rmxyadd  42910  jm2.25  42988  relexpmulnn  43699  binomcxplemnotnn0  44352  sumnnodd  45586  dvnmul  45899  stoweidlem13  45969  wallispilem4  46024  wallispi2lem1  46027  wallispi2lem2  46028  stirlinglem1  46030  stirlinglem6  46035  stirlinglem7  46036  stirlinglem8  46037  stirlinglem10  46039  dirkerper  46052  dirkertrigeqlem1  46054  dirkertrigeqlem2  46055  dirkertrigeqlem3  46056  fourierdlem83  46145  hoidmvlelem2  46552  hspmbllem1  46582  smfmullem1  46747  deccarry  47261  fmtnorec4  47474  mod42tp1mod8  47527  lighneallem3  47532  opoeALTV  47608  opeoALTV  47609  2zlidl  48084  2zrngamgm  48089  altgsumbcALT  48198  itcovalpclem2  48521  ackval2  48532  affinecomb2  48553  itscnhlc0yqe  48609  itsclc0yqsollem1  48612  itsclc0yqsol  48614  itscnhlc0xyqsol  48615  itsclc0xyqsolr  48619  itscnhlinecirc02plem1  48632