Theorem adddid 10403

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  (class class class)co 6924  ℂcc 10272   + caddc 10277   · cmul 10279

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1073

This theorem is referenced by:  addid1  10558  cnegex  10559  addcom  10564  addcomd  10580  subdi  10810  conjmul  11094  cju  11374  flhalf  12954  modcyc  13028  addmodlteq  13068  binom3  13308  sqoddm1div8  13353  bcpasc  13430  hashf1lem2  13558  remim  14268  mulre  14272  readd  14277  remullem  14279  imadd  14285  cjadd  14292  sqreulem  14510  iseraltlem2  14825  o1fsum  14953  binomlem  14969  climcndslem2  14990  binomfallfaclem2  15177  bpoly4  15196  tanval3  15270  sinadd  15300  tanadd  15303  dvdsmulgcd  15684  lcmgcdlem  15729  pythagtriplem1  15929  pcaddlem  16000  prmreclem4  16031  prmreclem6  16033  mul4sqlem  16065  vdwlem3  16095  vdwlem6  16098  vdwlem9  16101  nn0srg  20216  rge0srg  20217  icopnfcnv  23153  pcoass  23235  cphipval2  23451  minveclem2  23636  pjthlem1  23647  ovolunlem1a  23704  ovolscalem1  23721  itgcnlem  23997  itgadd  24032  itgmulc2  24041  itgsplit  24043  aaliou3lem2  24539  abelthlem7  24633  tangtx  24699  efgh  24729  tanarg  24806  logcnlem4  24832  mulcxp  24872  cxpmul2  24876  heron  25020  quad2  25021  dcubic1lem  25025  dcubic2  25026  mcubic  25029  binom4  25032  quart1  25038  atanlogsublem  25097  2efiatan  25100  lgamgulmlem3  25213  basellem2  25264  basellem3  25265  basellem8  25270  chtub  25393  bposlem9  25473  lgseisenlem2  25557  2lgsoddprmlem2  25590  2sqlem4  25602  2sqlem8  25607  dchrisumlem1  25634  dchrvmasum2if  25642  dchrisum0re  25658  mulog2sumlem1  25679  selberglem1  25690  selberglem2  25691  selberg  25693  selberg2  25696  chpdifbndlem1  25698  selberg3lem1  25702  selberg4  25706  pntsval2  25721  pntibndlem2  25736  pntlemr  25747  pntlemf  25750  pntlemo  25752  ostth2lem2  25779  ostth2lem3  25780  brbtwn2  26258  axsegconlem9  26278  axpasch  26294  axeuclidlem  26315  axcontlem2  26318  axcontlem4  26320  axcontlem7  26323  axcontlem8  26324  finsumvtxdg2ssteplem4  26900  ipasslem2  28263  minvecolem2  28307  pjhthlem1  28826  circlemeth  31324  subfacval2  31772  subfaclim  31773  faclimlem1  32227  itgaddnc  34100  itgmulc2nc  34108  dvasin  34126  resubdi  38208  pellexlem6  38368  pell1234qrmulcl  38389  rmxyadd  38455  jm2.25  38535  relexpmulnn  38968  binomcxplemnotnn0  39521  sumnnodd  40780  dvnmul  41096  stoweidlem13  41167  wallispilem4  41222  wallispi2lem1  41225  wallispi2lem2  41226  stirlinglem1  41228  stirlinglem6  41233  stirlinglem7  41234  stirlinglem8  41235  stirlinglem10  41237  dirkerper  41250  dirkertrigeqlem1  41252  dirkertrigeqlem2  41253  dirkertrigeqlem3  41254  fourierdlem83  41343  hoidmvlelem2  41747  hspmbllem1  41777  smfmullem1  41935  deccarry  42363  fmtnorec4  42492  mod42tp1mod8  42550  lighneallem3  42555  opoeALTV  42629  opeoALTV  42630  2zlidl  42959  2zrngamgm  42964  altgsumbcALT  43156  affinecomb2  43449  itscnhlc0yqe  43505  itsclc0yqsollem1  43508  itsclc0yqsol  43510  itscnhlc0xyqsol  43511  itsclc0xyqsolr  43515  itscnhlinecirc02plem1  43528