MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adddid Structured version   Visualization version   GIF version

Theorem adddid 10049
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
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 adddi 10010 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1324 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  (class class class)co 6635  cc 9919   + caddc 9924   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9988
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  addid1  10201  cnegex  10202  addcom  10207  addcomd  10223  subdi  10448  conjmul  10727  cju  11001  flhalf  12614  modcyc  12688  addmodlteq  12728  binom3  12968  sqoddm1div8  13011  bcpasc  13091  hashf1lem2  13223  remim  13838  mulre  13842  readd  13847  remullem  13849  imadd  13855  cjadd  13862  sqreulem  14080  iseraltlem2  14394  o1fsum  14526  binomlem  14542  climcndslem2  14563  binomfallfaclem2  14752  bpoly4  14771  tanval3  14845  sinadd  14875  tanadd  14878  dvdsmulgcd  15255  lcmgcdlem  15300  pythagtriplem1  15502  pcaddlem  15573  prmreclem4  15604  prmreclem6  15606  mul4sqlem  15638  vdwlem3  15668  vdwlem6  15671  vdwlem9  15674  nn0srg  19797  rge0srg  19798  icopnfcnv  22722  pcoass  22805  cphipval2  23021  minveclem2  23178  pjthlem1  23189  ovolunlem1a  23245  ovolscalem1  23262  itgcnlem  23537  itgadd  23572  itgmulc2  23581  itgsplit  23583  aaliou3lem2  24079  abelthlem7  24173  tangtx  24238  efgh  24268  tanarg  24346  logcnlem4  24372  mulcxp  24412  cxpmul2  24416  heron  24546  quad2  24547  dcubic1lem  24551  dcubic2  24552  mcubic  24555  binom4  24558  quart1  24564  atanlogsublem  24623  2efiatan  24626  lgamgulmlem3  24738  basellem2  24789  basellem3  24790  basellem8  24795  chtub  24918  bposlem9  24998  lgseisenlem2  25082  2lgsoddprmlem2  25115  2sqlem4  25127  2sqlem8  25132  dchrisumlem1  25159  dchrvmasum2if  25167  dchrisum0re  25183  mulog2sumlem1  25204  selberglem1  25215  selberglem2  25216  selberg  25218  selberg2  25221  chpdifbndlem1  25223  selberg3lem1  25227  selberg4  25231  pntsval2  25246  pntibndlem2  25261  pntlemr  25272  pntlemf  25275  pntlemo  25277  ostth2lem2  25304  ostth2lem3  25305  brbtwn2  25766  axsegconlem9  25786  axpasch  25802  axeuclidlem  25823  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  axcontlem8  25832  finsumvtxdg2ssteplem4  26425  ipasslem2  27657  minvecolem2  27701  pjhthlem1  28220  circlemeth  30692  subfacval2  31143  subfaclim  31144  faclimlem1  31604  itgaddnc  33441  itgmulc2nc  33449  dvasin  33467  pellexlem6  37217  pell1234qrmulcl  37238  rmxyadd  37305  jm2.25  37385  relexpmulnn  37820  binomcxplemnotnn0  38375  sumnnodd  39662  dvnmul  39921  stoweidlem13  39993  wallispilem4  40048  wallispi2lem1  40051  wallispi2lem2  40052  stirlinglem1  40054  stirlinglem6  40059  stirlinglem7  40060  stirlinglem8  40061  stirlinglem10  40063  dirkerper  40076  dirkertrigeqlem1  40078  dirkertrigeqlem2  40079  dirkertrigeqlem3  40080  fourierdlem83  40169  hoidmvlelem2  40573  hspmbllem1  40603  smfmullem1  40761  deccarry  41084  fmtnorec4  41226  mod42tp1mod8  41284  lighneallem3  41289  opoeALTV  41359  opeoALTV  41360  2zlidl  41699  2zrngamgm  41704  altgsumbcALT  41896
  Copyright terms: Public domain W3C validator