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

Theorem adddid 10276
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 10237 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1477 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6814  cc 10146   + caddc 10151   · cmul 10153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10215
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  addid1  10428  cnegex  10429  addcom  10434  addcomd  10450  subdi  10675  conjmul  10954  cju  11228  flhalf  12845  modcyc  12919  addmodlteq  12959  binom3  13199  sqoddm1div8  13242  bcpasc  13322  hashf1lem2  13452  remim  14076  mulre  14080  readd  14085  remullem  14087  imadd  14093  cjadd  14100  sqreulem  14318  iseraltlem2  14632  o1fsum  14764  binomlem  14780  climcndslem2  14801  binomfallfaclem2  14990  bpoly4  15009  tanval3  15083  sinadd  15113  tanadd  15116  dvdsmulgcd  15496  lcmgcdlem  15541  pythagtriplem1  15743  pcaddlem  15814  prmreclem4  15845  prmreclem6  15847  mul4sqlem  15879  vdwlem3  15909  vdwlem6  15912  vdwlem9  15915  nn0srg  20038  rge0srg  20039  icopnfcnv  22962  pcoass  23044  cphipval2  23260  minveclem2  23417  pjthlem1  23428  ovolunlem1a  23484  ovolscalem1  23501  itgcnlem  23775  itgadd  23810  itgmulc2  23819  itgsplit  23821  aaliou3lem2  24317  abelthlem7  24411  tangtx  24477  efgh  24507  tanarg  24585  logcnlem4  24611  mulcxp  24651  cxpmul2  24655  heron  24785  quad2  24786  dcubic1lem  24790  dcubic2  24791  mcubic  24794  binom4  24797  quart1  24803  atanlogsublem  24862  2efiatan  24865  lgamgulmlem3  24977  basellem2  25028  basellem3  25029  basellem8  25034  chtub  25157  bposlem9  25237  lgseisenlem2  25321  2lgsoddprmlem2  25354  2sqlem4  25366  2sqlem8  25371  dchrisumlem1  25398  dchrvmasum2if  25406  dchrisum0re  25422  mulog2sumlem1  25443  selberglem1  25454  selberglem2  25455  selberg  25457  selberg2  25460  chpdifbndlem1  25462  selberg3lem1  25466  selberg4  25470  pntsval2  25485  pntibndlem2  25500  pntlemr  25511  pntlemf  25514  pntlemo  25516  ostth2lem2  25543  ostth2lem3  25544  brbtwn2  26005  axsegconlem9  26025  axpasch  26041  axeuclidlem  26062  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  axcontlem8  26071  finsumvtxdg2ssteplem4  26675  ipasslem2  28017  minvecolem2  28061  pjhthlem1  28580  circlemeth  31048  subfacval2  31497  subfaclim  31498  faclimlem1  31957  itgaddnc  33801  itgmulc2nc  33809  dvasin  33827  pellexlem6  37918  pell1234qrmulcl  37939  rmxyadd  38006  jm2.25  38086  relexpmulnn  38521  binomcxplemnotnn0  39075  sumnnodd  40383  dvnmul  40679  stoweidlem13  40751  wallispilem4  40806  wallispi2lem1  40809  wallispi2lem2  40810  stirlinglem1  40812  stirlinglem6  40817  stirlinglem7  40818  stirlinglem8  40819  stirlinglem10  40821  dirkerper  40834  dirkertrigeqlem1  40836  dirkertrigeqlem2  40837  dirkertrigeqlem3  40838  fourierdlem83  40927  hoidmvlelem2  41334  hspmbllem1  41364  smfmullem1  41522  deccarry  41849  fmtnorec4  41989  mod42tp1mod8  42047  lighneallem3  42052  opoeALTV  42122  opeoALTV  42123  2zlidl  42462  2zrngamgm  42467  altgsumbcALT  42659
  Copyright terms: Public domain W3C validator