Theorem adddid 11238

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113   · cmul 11115

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090

This theorem is referenced by:  addrid  11394  cnegex  11395  addcom  11400  addcomd  11416  subdi  11647  conjmul  11931  cju  12208  flhalf  13795  modcyc  13871  addmodlteq  13911  binom3  14187  sqoddm1div8  14206  bcpasc  14281  hashf1lem2  14417  remim  15064  mulre  15068  readd  15073  remullem  15075  imadd  15081  cjadd  15088  sqreulem  15306  iseraltlem2  15629  o1fsum  15759  binomlem  15775  climcndslem2  15796  binomfallfaclem2  15984  bpoly4  16003  tanval3  16077  sinadd  16107  tanadd  16110  dvdsmulgcd  16497  lcmgcdlem  16543  pythagtriplem1  16749  pcaddlem  16821  prmreclem4  16852  prmreclem6  16854  mul4sqlem  16886  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  nn0srg  21015  rge0srg  21016  mhppwdeg  21693  icopnfcnv  24458  pcoass  24540  cphipval2  24758  minveclem2  24943  pjthlem1  24954  ovolunlem1a  25013  ovolscalem1  25030  itgcnlem  25307  itgadd  25342  itgmulc2  25351  itgsplit  25353  aaliou3lem2  25856  abelthlem7  25950  tangtx  26015  efgh  26050  tanarg  26127  logcnlem4  26153  mulcxp  26193  cxpmul2  26197  heron  26343  quad2  26344  dcubic1lem  26348  dcubic2  26349  mcubic  26352  binom4  26355  quart1  26361  atanlogsublem  26420  2efiatan  26423  lgamgulmlem3  26535  basellem2  26586  basellem3  26587  basellem8  26592  chtub  26715  bposlem9  26795  lgseisenlem2  26879  2lgsoddprmlem2  26912  2sqlem4  26924  2sqlem8  26929  dchrisumlem1  26992  dchrvmasum2if  27000  dchrisum0re  27016  mulog2sumlem1  27037  selberglem1  27048  selberglem2  27049  selberg  27051  selberg2  27054  chpdifbndlem1  27056  selberg3lem1  27060  selberg4  27064  pntsval2  27079  pntibndlem2  27094  pntlemr  27105  pntlemf  27108  pntlemo  27110  ostth2lem2  27137  ostth2lem3  27138  brbtwn2  28194  axsegconlem9  28214  axpasch  28230  axeuclidlem  28251  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  finsumvtxdg2ssteplem4  28836  ipasslem2  30116  minvecolem2  30159  pjhthlem1  30675  wrdt2ind  32148  ccfldsrarelvec  32776  circlemeth  33683  subfacval2  34209  subfaclim  34210  faclimlem1  34744  itgaddnc  36596  itgmulc2nc  36604  dvasin  36620  2np3bcnp1  41008  nnadddir  41232  nnmul1com  41233  nnmulcom  41234  sumcubes  41259  resubdi  41317  sn-negex12  41337  sn-mul01  41346  sn-mullid  41356  sn-0tie0  41360  sn-mul02  41361  renegmulnnass  41374  cnreeu  41389  fltmul  41425  cu3addd  41466  3cubeslem3l  41472  3cubeslem3r  41473  pellexlem6  41620  pell1234qrmulcl  41641  rmxyadd  41708  jm2.25  41786  relexpmulnn  42508  binomcxplemnotnn0  43163  sumnnodd  44394  dvnmul  44707  stoweidlem13  44777  wallispilem4  44832  wallispi2lem1  44835  wallispi2lem2  44836  stirlinglem1  44838  stirlinglem6  44843  stirlinglem7  44844  stirlinglem8  44845  stirlinglem10  44847  dirkerper  44860  dirkertrigeqlem1  44862  dirkertrigeqlem2  44863  dirkertrigeqlem3  44864  fourierdlem83  44953  hoidmvlelem2  45360  hspmbllem1  45390  smfmullem1  45555  deccarry  46067  fmtnorec4  46265  mod42tp1mod8  46318  lighneallem3  46323  opoeALTV  46399  opeoALTV  46400  2zlidl  46880  2zrngamgm  46885  altgsumbcALT  47077  itcovalpclem2  47405  ackval2  47416  affinecomb2  47437  itscnhlc0yqe  47493  itsclc0yqsollem1  47496  itsclc0yqsol  47498  itscnhlc0xyqsol  47499  itsclc0xyqsolr  47503  itscnhlinecirc02plem1  47516