Theorem adddid 11169

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041   · cmul 11043

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

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

This theorem is referenced by:  addrid  11326  cnegex  11327  addcom  11332  addcomd  11348  subdi  11583  conjmul  11872  cju  12155  nnadddir  12233  nnmul1com  12234  nnmulcom  12235  flhalf  13789  modcyc  13865  addmodlteq  13908  binom3  14186  sqoddm1div8  14205  bcpasc  14283  hashf1lem2  14418  remim  15079  mulre  15083  readd  15088  remullem  15090  imadd  15096  cjadd  15103  sqreulem  15322  iseraltlem2  15645  o1fsum  15776  binomlem  15794  climcndslem2  15815  binomfallfaclem2  16005  bpoly4  16024  tanval3  16101  sinadd  16131  tanadd  16134  dvdsmulgcd  16525  lcmgcdlem  16575  pythagtriplem1  16787  pcaddlem  16859  prmreclem4  16890  prmreclem6  16892  mul4sqlem  16924  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  nn0srg  21417  rge0srg  21418  mhppwdeg  22116  icopnfcnv  24909  pcoass  24991  cphipval2  25208  minveclem2  25393  pjthlem1  25404  ovolunlem1a  25463  ovolscalem1  25480  itgcnlem  25757  itgadd  25792  itgmulc2  25801  itgsplit  25803  aaliou3lem2  26309  abelthlem7  26403  tangtx  26469  efgh  26505  tanarg  26583  logcnlem4  26609  mulcxp  26649  cxpmul2  26653  heron  26802  quad2  26803  dcubic1lem  26807  dcubic2  26808  mcubic  26811  binom4  26814  quart1  26820  atanlogsublem  26879  2efiatan  26882  lgamgulmlem3  26994  basellem2  27045  basellem3  27046  basellem8  27051  chtub  27175  bposlem9  27255  lgseisenlem2  27339  2lgsoddprmlem2  27372  2sqlem4  27384  2sqlem8  27389  dchrisumlem1  27452  dchrvmasum2if  27460  dchrisum0re  27476  mulog2sumlem1  27497  selberglem1  27508  selberglem2  27509  selberg  27511  selberg2  27514  chpdifbndlem1  27516  selberg3lem1  27520  selberg4  27524  pntsval2  27539  pntibndlem2  27554  pntlemr  27565  pntlemf  27568  pntlemo  27570  ostth2lem2  27597  ostth2lem3  27598  brbtwn2  28974  axsegconlem9  28994  axpasch  29010  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  finsumvtxdg2ssteplem4  29617  ipasslem2  30903  minvecolem2  30946  pjhthlem1  31462  wrdt2ind  33013  ccfldsrarelvec  33815  constrrtcclem  33878  constrremulcl  33911  constrrecl  33913  circlemeth  34784  subfacval2  35369  subfaclim  35370  faclimlem1  35925  itgaddnc  38001  itgmulc2nc  38009  dvasin  38025  posbezout  42539  2np3bcnp1  42583  sumcubes  42745  resubdi  42828  sn-negex12  42849  sn-mul01  42858  sn-mullid  42868  redivdird  42894  sn-0tie0  42896  sn-mul02  42897  renegmulnnass  42910  cnreeu  42935  fltmul  43068  cu3addd  43113  3cubeslem3l  43118  3cubeslem3r  43119  pellexlem6  43262  pell1234qrmulcl  43283  rmxyadd  43349  jm2.25  43427  relexpmulnn  44136  binomcxplemnotnn0  44783  sumnnodd  46060  dvnmul  46371  stoweidlem13  46441  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem1  46502  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  fourierdlem83  46617  hoidmvlelem2  47024  hspmbllem1  47054  smfmullem1  47219  sin5tlem4  47324  deccarry  47759  fmtnorec4  48012  mod42tp1mod8  48065  lighneallem3  48070  opoeALTV  48159  opeoALTV  48160  2zlidl  48716  2zrngamgm  48721  altgsumbcALT  48829  itcovalpclem2  49147  ackval2  49158  affinecomb2  49179  itscnhlc0yqe  49235  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itsclc0xyqsolr  49245  itscnhlinecirc02plem1  49258