Theorem adddid 11363

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7446  ℂcc 11228   + caddc 11233   · cmul 11235

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

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

This theorem is used by:  addrid  11520  cnegex  11521  addcom  11526  addcomd  11542  subdi  11779  conjmul  12064  cju  12346  nnadddir  12424  nnmul1com  12425  nnmulcom  12426  flhalf  14000  modcyc  14076  addmodlteq  14119  binom3  14398  sqoddm1div8  14417  bcpasc  14495  hashf1lem2  14631  remim  15316  mulre  15320  readd  15325  remullem  15327  imadd  15333  cjadd  15340  sqreulem  15559  iseraltlem2  15882  o1fsum  16012  binomlem  16030  climcndslem2  16051  binomfallfaclem2  16238  bpoly4  16257  tanval3  16334  sinadd  16364  tanadd  16367  dvdsmulgcd  16762  lcmgcdlem  16813  pythagtriplem1  17026  pcaddlem  17098  prmreclem4  17129  prmreclem6  17131  mul4sqlem  17163  vdwlem3  17193  vdwlem6  17196  vdwlem9  17199  nn0srg  21776  rge0srg  21777  mhppwdeg  22504  icopnfcnv  25296  pcoass  25378  cphipval2  25595  minveclem2  25780  pjthlem1  25791  ovolunlem1a  25850  ovolscalem1  25867  itgcnlem  26143  itgadd  26178  itgmulc2  26187  itgsplit  26189  aaliou3lem2  26703  abelthlem7  26798  tangtx  26867  efgh  26902  tanarg  26980  logcnlem4  27006  mulcxp  27046  cxpmul2  27050  heron  27199  quad2  27200  dcubic1lem  27204  dcubic2  27205  mcubic  27208  binom4  27211  quart1  27217  atanlogsublem  27276  2efiatan  27279  lgamgulmlem3  27391  basellem2  27442  basellem3  27443  basellem8  27448  chtub  27572  bposlem9  27652  lgseisenlem2  27736  2lgsoddprmlem2  27769  2sqlem4  27781  2sqlem8  27786  dchrisumlem1  27849  dchrvmasum2if  27857  dchrisum0re  27873  mulog2sumlem1  27894  selberglem1  27905  selberglem2  27906  selberg  27908  selberg2  27911  chpdifbndlem1  27913  selberg3lem1  27917  selberg4  27921  pntsval2  27936  pntibndlem2  27951  pntlemr  27962  pntlemf  27965  pntlemo  27967  ostth2lem2  27994  ostth2lem3  27995  brbtwn2  29516  axsegconlem9  29536  axpasch  29552  axeuclidlem  29573  axcontlem2  29576  axcontlem4  29578  axcontlem7  29581  axcontlem8  29582  finsumvtxdg2ssteplem4  30162  ipasslem2  31467  minvecolem2  31510  pjhthlem1  32026  wrdt2ind  33589  ccfldsrarelvec  34386  constrrtcclem  34449  constrremulcl  34482  constrrecl  34484  circlemeth  35352  subfacval2  36132  subfaclim  36133  faclimlem1  36699  itgaddnc  38803  itgmulc2nc  38811  dvasin  38827  posbezout  43353  2np3bcnp1  43397  quadfac  43458  sumcubes  43574  resubdi  43651  sn-negex12  43672  sn-mul01  43681  sn-mullid  43691  redivdird  43717  sn-0tie0  43719  sn-mul02  43720  renegmulnnass  43733  cnreeu  43758  fltmul  43875  cu3addd  43895  3cubeslem3l  43900  3cubeslem3r  43901  pellexlem6  44045  pell1234qrmulcl  44066  rmxyadd  44132  jm2.25  44210  relexpmulnn  44912  binomcxplemnotnn0  45543  sumnnodd  46857  dvnmul  47168  stoweidlem13  47238  wallispilem4  47293  wallispi2lem1  47296  wallispi2lem2  47297  stirlinglem1  47299  stirlinglem6  47304  stirlinglem7  47305  stirlinglem8  47306  stirlinglem10  47308  dirkerper  47321  dirkertrigeqlem1  47323  dirkertrigeqlem2  47324  dirkertrigeqlem3  47325  fourierdlem83  47414  hoidmvlelem2  47821  hspmbllem1  47851  smfmullem1  48016  sin5tlem4  48137  deccarry  48596  fmtnorec4  48849  mod42tp1mod8  48902  lighneallem3  48907  opoeALTV  48996  opeoALTV  48997  2zlidl  49552  2zrngamgm  49557  altgsumbcALT  49680  itcovalpclem2  49998  ackval2  50009  affinecomb2  50030  itscnhlc0yqe  50086  itsclc0yqsollem1  50089  itsclc0yqsol  50091  itscnhlc0xyqsol  50092  itsclc0xyqsolr  50096  itscnhlinecirc02plem1  50109