Theorem adddid 11145

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7354  ℂcc 11013   + caddc 11018   · cmul 11020

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

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

This theorem is referenced by:  addrid  11302  cnegex  11303  addcom  11308  addcomd  11324  subdi  11559  conjmul  11847  cju  12130  flhalf  13738  modcyc  13814  addmodlteq  13857  binom3  14135  sqoddm1div8  14154  bcpasc  14232  hashf1lem2  14367  remim  15028  mulre  15032  readd  15037  remullem  15039  imadd  15045  cjadd  15052  sqreulem  15271  iseraltlem2  15594  o1fsum  15724  binomlem  15740  climcndslem2  15761  binomfallfaclem2  15951  bpoly4  15970  tanval3  16047  sinadd  16077  tanadd  16080  dvdsmulgcd  16471  lcmgcdlem  16521  pythagtriplem1  16732  pcaddlem  16804  prmreclem4  16835  prmreclem6  16837  mul4sqlem  16869  vdwlem3  16899  vdwlem6  16902  vdwlem9  16905  nn0srg  21378  rge0srg  21379  mhppwdeg  22068  icopnfcnv  24870  pcoass  24954  cphipval2  25171  minveclem2  25356  pjthlem1  25367  ovolunlem1a  25427  ovolscalem1  25444  itgcnlem  25721  itgadd  25756  itgmulc2  25765  itgsplit  25767  aaliou3lem2  26281  abelthlem7  26378  tangtx  26444  efgh  26480  tanarg  26558  logcnlem4  26584  mulcxp  26624  cxpmul2  26628  heron  26778  quad2  26779  dcubic1lem  26783  dcubic2  26784  mcubic  26787  binom4  26790  quart1  26796  atanlogsublem  26855  2efiatan  26858  lgamgulmlem3  26971  basellem2  27022  basellem3  27023  basellem8  27028  chtub  27153  bposlem9  27233  lgseisenlem2  27317  2lgsoddprmlem2  27350  2sqlem4  27362  2sqlem8  27367  dchrisumlem1  27430  dchrvmasum2if  27438  dchrisum0re  27454  mulog2sumlem1  27475  selberglem1  27486  selberglem2  27487  selberg  27489  selberg2  27492  chpdifbndlem1  27494  selberg3lem1  27498  selberg4  27502  pntsval2  27517  pntibndlem2  27532  pntlemr  27543  pntlemf  27546  pntlemo  27548  ostth2lem2  27575  ostth2lem3  27576  brbtwn2  28887  axsegconlem9  28907  axpasch  28923  axeuclidlem  28944  axcontlem2  28947  axcontlem4  28949  axcontlem7  28952  axcontlem8  28953  finsumvtxdg2ssteplem4  29531  ipasslem2  30816  minvecolem2  30859  pjhthlem1  31375  wrdt2ind  32943  ccfldsrarelvec  33707  constrrtcclem  33770  constrremulcl  33803  constrrecl  33805  circlemeth  34676  subfacval2  35254  subfaclim  35255  faclimlem1  35810  itgaddnc  37743  itgmulc2nc  37751  dvasin  37767  posbezout  42216  2np3bcnp1  42260  nnadddir  42391  nnmul1com  42392  nnmulcom  42393  sumcubes  42434  resubdi  42517  sn-negex12  42538  sn-mul01  42547  sn-mullid  42557  sn-0tie0  42572  sn-mul02  42573  renegmulnnass  42586  cnreeu  42611  fltmul  42756  cu3addd  42801  3cubeslem3l  42806  3cubeslem3r  42807  pellexlem6  42954  pell1234qrmulcl  42975  rmxyadd  43041  jm2.25  43119  relexpmulnn  43829  binomcxplemnotnn0  44476  sumnnodd  45757  dvnmul  46068  stoweidlem13  46138  wallispilem4  46193  wallispi2lem1  46196  wallispi2lem2  46197  stirlinglem1  46199  stirlinglem6  46204  stirlinglem7  46205  stirlinglem8  46206  stirlinglem10  46208  dirkerper  46221  dirkertrigeqlem1  46223  dirkertrigeqlem2  46224  dirkertrigeqlem3  46225  fourierdlem83  46314  hoidmvlelem2  46721  hspmbllem1  46751  smfmullem1  46916  deccarry  47438  fmtnorec4  47676  mod42tp1mod8  47729  lighneallem3  47734  opoeALTV  47810  opeoALTV  47811  2zlidl  48367  2zrngamgm  48372  altgsumbcALT  48480  itcovalpclem2  48799  ackval2  48810  affinecomb2  48831  itscnhlc0yqe  48887  itsclc0yqsollem1  48890  itsclc0yqsol  48892  itscnhlc0xyqsol  48893  itsclc0xyqsolr  48897  itscnhlinecirc02plem1  48910