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

Theorem adddid 9917
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 9878 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6524  cc 9787   + caddc 9792   · cmul 9794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9856
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032
This theorem is referenced by:  addid1  10064  cnegex  10065  addcom  10070  addcomd  10086  subdi  10311  conjmul  10588  cju  10860  flhalf  12445  modcyc  12519  addmodlteq  12559  binom3  12799  sqoddm1div8  12842  bcpasc  12922  hashf1lem2  13046  remim  13648  mulre  13652  readd  13657  remullem  13659  imadd  13665  cjadd  13672  sqreulem  13890  iseraltlem2  14204  o1fsum  14329  binomlem  14343  climcndslem2  14364  binomfallfaclem2  14553  bpoly4  14572  tanval3  14646  sinadd  14676  tanadd  14679  dvdsmulgcd  15055  lcmgcdlem  15100  pythagtriplem1  15302  pcaddlem  15373  prmreclem4  15404  prmreclem6  15406  mul4sqlem  15438  vdwlem3  15468  vdwlem6  15471  vdwlem9  15474  nn0srg  19578  rge0srg  19579  icopnfcnv  22477  pcoass  22560  minveclem2  22919  pjthlem1  22930  ovolunlem1a  22985  ovolscalem1  23002  itgcnlem  23276  itgadd  23311  itgmulc2  23320  itgsplit  23322  aaliou3lem2  23816  abelthlem7  23910  tangtx  23975  efgh  24005  tanarg  24083  logcnlem4  24105  mulcxp  24145  cxpmul2  24149  heron  24279  quad2  24280  dcubic1lem  24284  dcubic2  24285  mcubic  24288  binom4  24291  quart1  24297  atanlogsublem  24356  2efiatan  24359  lgamgulmlem3  24471  basellem2  24522  basellem3  24523  basellem8  24528  chtub  24651  bposlem9  24731  lgseisenlem2  24815  2lgsoddprmlem2  24848  2sqlem4  24860  2sqlem8  24865  dchrisumlem1  24892  dchrvmasum2if  24900  dchrisum0re  24916  mulog2sumlem1  24937  selberglem1  24948  selberglem2  24949  selberg  24951  selberg2  24954  chpdifbndlem1  24956  selberg3lem1  24960  selberg4  24964  pntsval2  24979  pntibndlem2  24994  pntlemr  25005  pntlemf  25008  pntlemo  25010  ostth2lem2  25037  ostth2lem3  25038  brbtwn2  25500  axsegconlem9  25520  axpasch  25536  axeuclidlem  25557  axcontlem2  25560  axcontlem4  25562  axcontlem7  25565  axcontlem8  25566  ipasslem2  26874  minvecolem2  26918  pjhthlem1  27437  subfacval2  30226  subfaclim  30227  faclimlem1  30685  itgaddnc  32440  itgmulc2nc  32448  dvasin  32466  pellexlem6  36216  pell1234qrmulcl  36237  rmxyadd  36304  jm2.25  36384  relexpmulnn  36820  binomcxplemnotnn0  37377  sumnnodd  38498  dvnmul  38634  stoweidlem13  38707  wallispilem4  38762  wallispi2lem1  38765  wallispi2lem2  38766  stirlinglem1  38768  stirlinglem6  38773  stirlinglem7  38774  stirlinglem8  38775  stirlinglem10  38777  dirkerper  38790  dirkertrigeqlem1  38792  dirkertrigeqlem2  38793  dirkertrigeqlem3  38794  fourierdlem83  38883  hoidmvlelem2  39287  hspmbllem1  39317  smfmullem1  39477  deccarry  39743  fmtnorec4  39801  mod42tp1mod8  39859  lighneallem3  39864  opoeALTV  39934  opeoALTV  39935  2zlidl  41723  2zrngamgm  41728  altgsumbcALT  41923
  Copyright terms: Public domain W3C validator