Theorem adddid 11264

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137   · cmul 11139

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

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

This theorem is referenced by:  addrid  11420  cnegex  11421  addcom  11426  addcomd  11442  subdi  11675  conjmul  11963  cju  12241  flhalf  13852  modcyc  13928  addmodlteq  13969  binom3  14247  sqoddm1div8  14266  bcpasc  14344  hashf1lem2  14479  remim  15141  mulre  15145  readd  15150  remullem  15152  imadd  15158  cjadd  15165  sqreulem  15383  iseraltlem2  15704  o1fsum  15834  binomlem  15850  climcndslem2  15871  binomfallfaclem2  16061  bpoly4  16080  tanval3  16157  sinadd  16187  tanadd  16190  dvdsmulgcd  16580  lcmgcdlem  16630  pythagtriplem1  16841  pcaddlem  16913  prmreclem4  16944  prmreclem6  16946  mul4sqlem  16978  vdwlem3  17008  vdwlem6  17011  vdwlem9  17014  nn0srg  21410  rge0srg  21411  mhppwdeg  22093  icopnfcnv  24896  pcoass  24980  cphipval2  25198  minveclem2  25383  pjthlem1  25394  ovolunlem1a  25454  ovolscalem1  25471  itgcnlem  25748  itgadd  25783  itgmulc2  25792  itgsplit  25794  aaliou3lem2  26308  abelthlem7  26405  tangtx  26471  efgh  26507  tanarg  26585  logcnlem4  26611  mulcxp  26651  cxpmul2  26655  heron  26805  quad2  26806  dcubic1lem  26810  dcubic2  26811  mcubic  26814  binom4  26817  quart1  26823  atanlogsublem  26882  2efiatan  26885  lgamgulmlem3  26998  basellem2  27049  basellem3  27050  basellem8  27055  chtub  27180  bposlem9  27260  lgseisenlem2  27344  2lgsoddprmlem2  27377  2sqlem4  27389  2sqlem8  27394  dchrisumlem1  27457  dchrvmasum2if  27465  dchrisum0re  27481  mulog2sumlem1  27502  selberglem1  27513  selberglem2  27514  selberg  27516  selberg2  27519  chpdifbndlem1  27521  selberg3lem1  27525  selberg4  27529  pntsval2  27544  pntibndlem2  27559  pntlemr  27570  pntlemf  27573  pntlemo  27575  ostth2lem2  27602  ostth2lem3  27603  brbtwn2  28889  axsegconlem9  28909  axpasch  28925  axeuclidlem  28946  axcontlem2  28949  axcontlem4  28951  axcontlem7  28954  axcontlem8  28955  finsumvtxdg2ssteplem4  29533  ipasslem2  30818  minvecolem2  30861  pjhthlem1  31377  wrdt2ind  32934  ccfldsrarelvec  33717  constrrtcclem  33773  constrremulcl  33806  constrrecl  33808  circlemeth  34677  subfacval2  35214  subfaclim  35215  faclimlem1  35765  itgaddnc  37709  itgmulc2nc  37717  dvasin  37733  posbezout  42118  2np3bcnp1  42162  nnadddir  42288  nnmul1com  42289  nnmulcom  42290  sumcubes  42331  resubdi  42414  sn-negex12  42434  sn-mul01  42443  sn-mullid  42453  sn-0tie0  42457  sn-mul02  42458  renegmulnnass  42471  cnreeu  42488  fltmul  42633  cu3addd  42679  3cubeslem3l  42684  3cubeslem3r  42685  pellexlem6  42832  pell1234qrmulcl  42853  rmxyadd  42920  jm2.25  42998  relexpmulnn  43708  binomcxplemnotnn0  44355  sumnnodd  45639  dvnmul  45952  stoweidlem13  46022  wallispilem4  46077  wallispi2lem1  46080  wallispi2lem2  46081  stirlinglem1  46083  stirlinglem6  46088  stirlinglem7  46089  stirlinglem8  46090  stirlinglem10  46092  dirkerper  46105  dirkertrigeqlem1  46107  dirkertrigeqlem2  46108  dirkertrigeqlem3  46109  fourierdlem83  46198  hoidmvlelem2  46605  hspmbllem1  46635  smfmullem1  46800  deccarry  47320  fmtnorec4  47543  mod42tp1mod8  47596  lighneallem3  47601  opoeALTV  47677  opeoALTV  47678  2zlidl  48195  2zrngamgm  48200  altgsumbcALT  48308  itcovalpclem2  48631  ackval2  48642  affinecomb2  48663  itscnhlc0yqe  48719  itsclc0yqsollem1  48722  itsclc0yqsol  48724  itscnhlc0xyqsol  48725  itsclc0xyqsolr  48729  itscnhlinecirc02plem1  48742