Theorem adddid 11167

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039   · cmul 11041

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  addrid  11324  cnegex  11325  addcom  11330  addcomd  11346  subdi  11581  conjmul  11870  cju  12153  nnadddir  12231  nnmul1com  12232  nnmulcom  12233  flhalf  13787  modcyc  13863  addmodlteq  13906  binom3  14184  sqoddm1div8  14203  bcpasc  14281  hashf1lem2  14416  remim  15077  mulre  15081  readd  15086  remullem  15088  imadd  15094  cjadd  15101  sqreulem  15320  iseraltlem2  15643  o1fsum  15774  binomlem  15792  climcndslem2  15813  binomfallfaclem2  16003  bpoly4  16022  tanval3  16099  sinadd  16129  tanadd  16132  dvdsmulgcd  16523  lcmgcdlem  16573  pythagtriplem1  16785  pcaddlem  16857  prmreclem4  16888  prmreclem6  16890  mul4sqlem  16922  vdwlem3  16952  vdwlem6  16955  vdwlem9  16958  nn0srg  21419  rge0srg  21420  mhppwdeg  22145  icopnfcnv  24934  pcoass  25016  cphipval2  25233  minveclem2  25418  pjthlem1  25429  ovolunlem1a  25488  ovolscalem1  25505  itgcnlem  25782  itgadd  25817  itgmulc2  25826  itgsplit  25828  aaliou3lem2  26334  abelthlem7  26428  tangtx  26494  efgh  26530  tanarg  26608  logcnlem4  26634  mulcxp  26674  cxpmul2  26678  heron  26827  quad2  26828  dcubic1lem  26832  dcubic2  26833  mcubic  26836  binom4  26839  quart1  26845  atanlogsublem  26904  2efiatan  26907  lgamgulmlem3  27019  basellem2  27070  basellem3  27071  basellem8  27076  chtub  27200  bposlem9  27280  lgseisenlem2  27364  2lgsoddprmlem2  27397  2sqlem4  27409  2sqlem8  27414  dchrisumlem1  27477  dchrvmasum2if  27485  dchrisum0re  27501  mulog2sumlem1  27522  selberglem1  27533  selberglem2  27534  selberg  27536  selberg2  27539  chpdifbndlem1  27541  selberg3lem1  27545  selberg4  27549  pntsval2  27564  pntibndlem2  27579  pntlemr  27590  pntlemf  27593  pntlemo  27595  ostth2lem2  27622  ostth2lem3  27623  brbtwn2  28999  axsegconlem9  29019  axpasch  29035  axeuclidlem  29056  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  axcontlem8  29065  finsumvtxdg2ssteplem4  29642  ipasslem2  30928  minvecolem2  30971  pjhthlem1  31487  wrdt2ind  33039  ccfldsrarelvec  33862  constrrtcclem  33925  constrremulcl  33958  constrrecl  33960  circlemeth  34831  subfacval2  35422  subfaclim  35423  faclimlem1  35978  itgaddnc  38054  itgmulc2nc  38062  dvasin  38078  posbezout  42592  2np3bcnp1  42636  sumcubes  42797  resubdi  42880  sn-negex12  42901  sn-mul01  42910  sn-mullid  42920  redivdird  42946  sn-0tie0  42948  sn-mul02  42949  renegmulnnass  42962  cnreeu  42987  fltmul  43092  cu3addd  43137  3cubeslem3l  43142  3cubeslem3r  43143  pellexlem6  43286  pell1234qrmulcl  43307  rmxyadd  43373  jm2.25  43451  relexpmulnn  44160  binomcxplemnotnn0  44807  sumnnodd  46082  dvnmul  46393  stoweidlem13  46463  wallispilem4  46518  wallispi2lem1  46521  wallispi2lem2  46522  stirlinglem1  46524  stirlinglem6  46529  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  dirkerper  46546  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  fourierdlem83  46639  hoidmvlelem2  47046  hspmbllem1  47076  smfmullem1  47241  sin5tlem4  47346  deccarry  47781  fmtnorec4  48034  mod42tp1mod8  48087  lighneallem3  48092  opoeALTV  48181  opeoALTV  48182  2zlidl  48738  2zrngamgm  48743  altgsumbcALT  48851  itcovalpclem2  49169  ackval2  49180  affinecomb2  49201  itscnhlc0yqe  49257  itsclc0yqsollem1  49260  itsclc0yqsol  49262  itscnhlc0xyqsol  49263  itsclc0xyqsolr  49267  itscnhlinecirc02plem1  49280