Theorem adddid 11168

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 7368  ℂ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  11325  cnegex  11326  addcom  11331  addcomd  11347  subdi  11582  conjmul  11870  cju  12153  flhalf  13762  modcyc  13838  addmodlteq  13881  binom3  14159  sqoddm1div8  14178  bcpasc  14256  hashf1lem2  14391  remim  15052  mulre  15056  readd  15061  remullem  15063  imadd  15069  cjadd  15076  sqreulem  15295  iseraltlem2  15618  o1fsum  15748  binomlem  15764  climcndslem2  15785  binomfallfaclem2  15975  bpoly4  15994  tanval3  16071  sinadd  16101  tanadd  16104  dvdsmulgcd  16495  lcmgcdlem  16545  pythagtriplem1  16756  pcaddlem  16828  prmreclem4  16859  prmreclem6  16861  mul4sqlem  16893  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  nn0srg  21404  rge0srg  21405  mhppwdeg  22105  icopnfcnv  24908  pcoass  24992  cphipval2  25209  minveclem2  25394  pjthlem1  25405  ovolunlem1a  25465  ovolscalem1  25482  itgcnlem  25759  itgadd  25794  itgmulc2  25803  itgsplit  25805  aaliou3lem2  26319  abelthlem7  26416  tangtx  26482  efgh  26518  tanarg  26596  logcnlem4  26622  mulcxp  26662  cxpmul2  26666  heron  26816  quad2  26817  dcubic1lem  26821  dcubic2  26822  mcubic  26825  binom4  26828  quart1  26834  atanlogsublem  26893  2efiatan  26896  lgamgulmlem3  27009  basellem2  27060  basellem3  27061  basellem8  27066  chtub  27191  bposlem9  27271  lgseisenlem2  27355  2lgsoddprmlem2  27388  2sqlem4  27400  2sqlem8  27405  dchrisumlem1  27468  dchrvmasum2if  27476  dchrisum0re  27492  mulog2sumlem1  27513  selberglem1  27524  selberglem2  27525  selberg  27527  selberg2  27530  chpdifbndlem1  27532  selberg3lem1  27536  selberg4  27540  pntsval2  27555  pntibndlem2  27570  pntlemr  27581  pntlemf  27584  pntlemo  27586  ostth2lem2  27613  ostth2lem3  27614  brbtwn2  28990  axsegconlem9  29010  axpasch  29026  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  finsumvtxdg2ssteplem4  29634  ipasslem2  30919  minvecolem2  30962  pjhthlem1  31478  wrdt2ind  33045  ccfldsrarelvec  33848  constrrtcclem  33911  constrremulcl  33944  constrrecl  33946  circlemeth  34817  subfacval2  35400  subfaclim  35401  faclimlem1  35956  itgaddnc  37928  itgmulc2nc  37936  dvasin  37952  posbezout  42467  2np3bcnp1  42511  nnadddir  42637  nnmul1com  42638  nnmulcom  42639  sumcubes  42680  resubdi  42763  sn-negex12  42784  sn-mul01  42793  sn-mullid  42803  sn-0tie0  42818  sn-mul02  42819  renegmulnnass  42832  cnreeu  42857  fltmul  42990  cu3addd  43035  3cubeslem3l  43040  3cubeslem3r  43041  pellexlem6  43188  pell1234qrmulcl  43209  rmxyadd  43275  jm2.25  43353  relexpmulnn  44062  binomcxplemnotnn0  44709  sumnnodd  45987  dvnmul  46298  stoweidlem13  46368  wallispilem4  46423  wallispi2lem1  46426  wallispi2lem2  46427  stirlinglem1  46429  stirlinglem6  46434  stirlinglem7  46435  stirlinglem8  46436  stirlinglem10  46438  dirkerper  46451  dirkertrigeqlem1  46453  dirkertrigeqlem2  46454  dirkertrigeqlem3  46455  fourierdlem83  46544  hoidmvlelem2  46951  hspmbllem1  46981  smfmullem1  47146  deccarry  47668  fmtnorec4  47906  mod42tp1mod8  47959  lighneallem3  47964  opoeALTV  48040  opeoALTV  48041  2zlidl  48597  2zrngamgm  48602  altgsumbcALT  48710  itcovalpclem2  49028  ackval2  49039  affinecomb2  49060  itscnhlc0yqe  49116  itsclc0yqsollem1  49119  itsclc0yqsol  49121  itscnhlc0xyqsol  49122  itsclc0xyqsolr  49126  itscnhlinecirc02plem1  49139