Theorem adddid 11198

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   · cmul 11073

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

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

This theorem is referenced by:  addrid  11354  cnegex  11355  addcom  11360  addcomd  11376  subdi  11611  conjmul  11899  cju  12182  flhalf  13792  modcyc  13868  addmodlteq  13911  binom3  14189  sqoddm1div8  14208  bcpasc  14286  hashf1lem2  14421  remim  15083  mulre  15087  readd  15092  remullem  15094  imadd  15100  cjadd  15107  sqreulem  15326  iseraltlem2  15649  o1fsum  15779  binomlem  15795  climcndslem2  15816  binomfallfaclem2  16006  bpoly4  16025  tanval3  16102  sinadd  16132  tanadd  16135  dvdsmulgcd  16526  lcmgcdlem  16576  pythagtriplem1  16787  pcaddlem  16859  prmreclem4  16890  prmreclem6  16892  mul4sqlem  16924  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  nn0srg  21354  rge0srg  21355  mhppwdeg  22037  icopnfcnv  24840  pcoass  24924  cphipval2  25141  minveclem2  25326  pjthlem1  25337  ovolunlem1a  25397  ovolscalem1  25414  itgcnlem  25691  itgadd  25726  itgmulc2  25735  itgsplit  25737  aaliou3lem2  26251  abelthlem7  26348  tangtx  26414  efgh  26450  tanarg  26528  logcnlem4  26554  mulcxp  26594  cxpmul2  26598  heron  26748  quad2  26749  dcubic1lem  26753  dcubic2  26754  mcubic  26757  binom4  26760  quart1  26766  atanlogsublem  26825  2efiatan  26828  lgamgulmlem3  26941  basellem2  26992  basellem3  26993  basellem8  26998  chtub  27123  bposlem9  27203  lgseisenlem2  27287  2lgsoddprmlem2  27320  2sqlem4  27332  2sqlem8  27337  dchrisumlem1  27400  dchrvmasum2if  27408  dchrisum0re  27424  mulog2sumlem1  27445  selberglem1  27456  selberglem2  27457  selberg  27459  selberg2  27462  chpdifbndlem1  27464  selberg3lem1  27468  selberg4  27472  pntsval2  27487  pntibndlem2  27502  pntlemr  27513  pntlemf  27516  pntlemo  27518  ostth2lem2  27545  ostth2lem3  27546  brbtwn2  28832  axsegconlem9  28852  axpasch  28868  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  finsumvtxdg2ssteplem4  29476  ipasslem2  30761  minvecolem2  30804  pjhthlem1  31320  wrdt2ind  32875  ccfldsrarelvec  33666  constrrtcclem  33724  constrremulcl  33757  constrrecl  33759  circlemeth  34631  subfacval2  35174  subfaclim  35175  faclimlem1  35730  itgaddnc  37674  itgmulc2nc  37682  dvasin  37698  posbezout  42088  2np3bcnp1  42132  nnadddir  42258  nnmul1com  42259  nnmulcom  42260  sumcubes  42301  resubdi  42384  sn-negex12  42405  sn-mul01  42414  sn-mullid  42424  sn-0tie0  42439  sn-mul02  42440  renegmulnnass  42453  cnreeu  42478  fltmul  42623  cu3addd  42669  3cubeslem3l  42674  3cubeslem3r  42675  pellexlem6  42822  pell1234qrmulcl  42843  rmxyadd  42910  jm2.25  42988  relexpmulnn  43698  binomcxplemnotnn0  44345  sumnnodd  45628  dvnmul  45941  stoweidlem13  46011  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem1  46072  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  fourierdlem83  46187  hoidmvlelem2  46594  hspmbllem1  46624  smfmullem1  46789  deccarry  47312  fmtnorec4  47550  mod42tp1mod8  47603  lighneallem3  47608  opoeALTV  47684  opeoALTV  47685  2zlidl  48228  2zrngamgm  48233  altgsumbcALT  48341  itcovalpclem2  48660  ackval2  48671  affinecomb2  48692  itscnhlc0yqe  48748  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itscnhlinecirc02plem1  48771