Theorem adddid 11314

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   + caddc 11184   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11471  cnegex  11472  addcom  11477  addcomd  11493  subdi  11730  conjmul  12015  cju  12297  nnadddir  12375  nnmul1com  12376  nnmulcom  12377  flhalf  13950  modcyc  14026  addmodlteq  14069  binom3  14348  sqoddm1div8  14367  bcpasc  14445  hashf1lem2  14581  remim  15264  mulre  15268  readd  15273  remullem  15275  imadd  15281  cjadd  15288  sqreulem  15507  iseraltlem2  15830  o1fsum  15960  binomlem  15978  climcndslem2  15999  binomfallfaclem2  16186  bpoly4  16205  tanval3  16282  sinadd  16312  tanadd  16315  dvdsmulgcd  16710  lcmgcdlem  16761  pythagtriplem1  16974  pcaddlem  17046  prmreclem4  17077  prmreclem6  17079  mul4sqlem  17111  vdwlem3  17141  vdwlem6  17144  vdwlem9  17147  nn0srg  21723  rge0srg  21724  mhppwdeg  22451  icopnfcnv  25243  pcoass  25325  cphipval2  25542  minveclem2  25727  pjthlem1  25738  ovolunlem1a  25797  ovolscalem1  25814  itgcnlem  26090  itgadd  26125  itgmulc2  26134  itgsplit  26136  aaliou3lem2  26652  abelthlem7  26747  tangtx  26816  efgh  26851  tanarg  26929  logcnlem4  26955  mulcxp  26995  cxpmul2  26999  heron  27148  quad2  27149  dcubic1lem  27153  dcubic2  27154  mcubic  27157  binom4  27160  quart1  27166  atanlogsublem  27225  2efiatan  27228  lgamgulmlem3  27340  basellem2  27391  basellem3  27392  basellem8  27397  chtub  27521  bposlem9  27601  lgseisenlem2  27685  2lgsoddprmlem2  27718  2sqlem4  27730  2sqlem8  27735  dchrisumlem1  27798  dchrvmasum2if  27806  dchrisum0re  27822  mulog2sumlem1  27843  selberglem1  27854  selberglem2  27855  selberg  27857  selberg2  27860  chpdifbndlem1  27862  selberg3lem1  27866  selberg4  27870  pntsval2  27885  pntibndlem2  27900  pntlemr  27911  pntlemf  27914  pntlemo  27916  ostth2lem2  27943  ostth2lem3  27944  brbtwn2  29465  axsegconlem9  29485  axpasch  29501  axeuclidlem  29522  axcontlem2  29525  axcontlem4  29527  axcontlem7  29530  axcontlem8  29531  finsumvtxdg2ssteplem4  30111  ipasslem2  31416  minvecolem2  31459  pjhthlem1  31975  wrdt2ind  33498  ccfldsrarelvec  34285  constrrtcclem  34348  constrremulcl  34381  constrrecl  34383  circlemeth  35252  subfacval2  35921  subfaclim  35922  faclimlem1  36477  itgaddnc  38566  itgmulc2nc  38574  dvasin  38590  posbezout  43118  2np3bcnp1  43162  quadfac  43223  sumcubes  43338  resubdi  43415  sn-negex12  43436  sn-mul01  43445  sn-mullid  43455  redivdird  43481  sn-0tie0  43483  sn-mul02  43484  renegmulnnass  43497  cnreeu  43522  fltmul  43625  cu3addd  43645  3cubeslem3l  43650  3cubeslem3r  43651  pellexlem6  43794  pell1234qrmulcl  43815  rmxyadd  43881  jm2.25  43959  relexpmulnn  44668  binomcxplemnotnn0  45299  sumnnodd  46586  dvnmul  46897  stoweidlem13  46967  wallispilem4  47022  wallispi2lem1  47025  wallispi2lem2  47026  stirlinglem1  47028  stirlinglem6  47033  stirlinglem7  47034  stirlinglem8  47035  stirlinglem10  47037  dirkerper  47050  dirkertrigeqlem1  47052  dirkertrigeqlem2  47053  dirkertrigeqlem3  47054  fourierdlem83  47143  hoidmvlelem2  47550  hspmbllem1  47580  smfmullem1  47745  sin5tlem4  47866  deccarry  48325  fmtnorec4  48578  mod42tp1mod8  48631  lighneallem3  48636  opoeALTV  48725  opeoALTV  48726  2zlidl  49281  2zrngamgm  49286  altgsumbcALT  49409  itcovalpclem2  49727  ackval2  49738  affinecomb2  49759  itscnhlc0yqe  49815  itsclc0yqsollem1  49818  itsclc0yqsol  49820  itscnhlc0xyqsol  49821  itsclc0xyqsolr  49825  itscnhlinecirc02plem1  49838