Theorem adddid 11160

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032   · cmul 11034

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

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

This theorem is referenced by:  addrid  11317  cnegex  11318  addcom  11323  addcomd  11339  subdi  11574  conjmul  11863  cju  12146  nnadddir  12224  nnmul1com  12225  nnmulcom  12226  flhalf  13780  modcyc  13856  addmodlteq  13899  binom3  14177  sqoddm1div8  14196  bcpasc  14274  hashf1lem2  14409  remim  15070  mulre  15074  readd  15079  remullem  15081  imadd  15087  cjadd  15094  sqreulem  15313  iseraltlem2  15636  o1fsum  15767  binomlem  15785  climcndslem2  15806  binomfallfaclem2  15996  bpoly4  16015  tanval3  16092  sinadd  16122  tanadd  16125  dvdsmulgcd  16516  lcmgcdlem  16566  pythagtriplem1  16778  pcaddlem  16850  prmreclem4  16881  prmreclem6  16883  mul4sqlem  16915  vdwlem3  16945  vdwlem6  16948  vdwlem9  16951  nn0srg  21427  rge0srg  21428  mhppwdeg  22126  icopnfcnv  24919  pcoass  25001  cphipval2  25218  minveclem2  25403  pjthlem1  25414  ovolunlem1a  25473  ovolscalem1  25490  itgcnlem  25767  itgadd  25802  itgmulc2  25811  itgsplit  25813  aaliou3lem2  26320  abelthlem7  26416  tangtx  26482  efgh  26518  tanarg  26596  logcnlem4  26622  mulcxp  26662  cxpmul2  26666  heron  26815  quad2  26816  dcubic1lem  26820  dcubic2  26821  mcubic  26824  binom4  26827  quart1  26833  atanlogsublem  26892  2efiatan  26895  lgamgulmlem3  27008  basellem2  27059  basellem3  27060  basellem8  27065  chtub  27189  bposlem9  27269  lgseisenlem2  27353  2lgsoddprmlem2  27386  2sqlem4  27398  2sqlem8  27403  dchrisumlem1  27466  dchrvmasum2if  27474  dchrisum0re  27490  mulog2sumlem1  27511  selberglem1  27522  selberglem2  27523  selberg  27525  selberg2  27528  chpdifbndlem1  27530  selberg3lem1  27534  selberg4  27538  pntsval2  27553  pntibndlem2  27568  pntlemr  27579  pntlemf  27582  pntlemo  27584  ostth2lem2  27611  ostth2lem3  27612  brbtwn2  28988  axsegconlem9  29008  axpasch  29024  axeuclidlem  29045  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  finsumvtxdg2ssteplem4  29632  ipasslem2  30918  minvecolem2  30961  pjhthlem1  31477  wrdt2ind  33028  ccfldsrarelvec  33831  constrrtcclem  33894  constrremulcl  33927  constrrecl  33929  circlemeth  34800  subfacval2  35385  subfaclim  35386  faclimlem1  35941  itgaddnc  38015  itgmulc2nc  38023  dvasin  38039  posbezout  42553  2np3bcnp1  42597  sumcubes  42759  resubdi  42842  sn-negex12  42863  sn-mul01  42872  sn-mullid  42882  redivdird  42908  sn-0tie0  42910  sn-mul02  42911  renegmulnnass  42924  cnreeu  42949  fltmul  43082  cu3addd  43127  3cubeslem3l  43132  3cubeslem3r  43133  pellexlem6  43280  pell1234qrmulcl  43301  rmxyadd  43367  jm2.25  43445  relexpmulnn  44154  binomcxplemnotnn0  44801  sumnnodd  46078  dvnmul  46389  stoweidlem13  46459  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem1  46520  stirlinglem6  46525  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  fourierdlem83  46635  hoidmvlelem2  47042  hspmbllem1  47072  smfmullem1  47237  sin5tlem4  47340  deccarry  47771  fmtnorec4  48024  mod42tp1mod8  48077  lighneallem3  48082  opoeALTV  48171  opeoALTV  48172  2zlidl  48728  2zrngamgm  48733  altgsumbcALT  48841  itcovalpclem2  49159  ackval2  49170  affinecomb2  49191  itscnhlc0yqe  49247  itsclc0yqsollem1  49250  itsclc0yqsol  49252  itscnhlc0xyqsol  49253  itsclc0xyqsolr  49257  itscnhlinecirc02plem1  49270