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

Theorem adddid 10659
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 10620 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1368 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7146  cc 10529   + caddc 10534   · cmul 10536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10598
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  addid1  10814  cnegex  10815  addcom  10820  addcomd  10836  subdi  11067  conjmul  11351  cju  11628  flhalf  13202  modcyc  13276  addmodlteq  13316  binom3  13588  sqoddm1div8  13607  bcpasc  13684  hashf1lem2  13817  remim  14474  mulre  14478  readd  14483  remullem  14485  imadd  14491  cjadd  14498  sqreulem  14717  iseraltlem2  15037  o1fsum  15166  binomlem  15182  climcndslem2  15203  binomfallfaclem2  15392  bpoly4  15411  tanval3  15485  sinadd  15515  tanadd  15518  dvdsmulgcd  15901  lcmgcdlem  15946  pythagtriplem1  16149  pcaddlem  16220  prmreclem4  16251  prmreclem6  16253  mul4sqlem  16285  vdwlem3  16315  vdwlem6  16318  vdwlem9  16321  nn0srg  20610  rge0srg  20611  icopnfcnv  23545  pcoass  23627  cphipval2  23843  minveclem2  24028  pjthlem1  24039  ovolunlem1a  24098  ovolscalem1  24115  itgcnlem  24391  itgadd  24426  itgmulc2  24435  itgsplit  24437  aaliou3lem2  24937  abelthlem7  25031  tangtx  25096  efgh  25131  tanarg  25208  logcnlem4  25234  mulcxp  25274  cxpmul2  25278  heron  25422  quad2  25423  dcubic1lem  25427  dcubic2  25428  mcubic  25431  binom4  25434  quart1  25440  atanlogsublem  25499  2efiatan  25502  lgamgulmlem3  25614  basellem2  25665  basellem3  25666  basellem8  25671  chtub  25794  bposlem9  25874  lgseisenlem2  25958  2lgsoddprmlem2  25991  2sqlem4  26003  2sqlem8  26008  dchrisumlem1  26071  dchrvmasum2if  26079  dchrisum0re  26095  mulog2sumlem1  26116  selberglem1  26127  selberglem2  26128  selberg  26130  selberg2  26133  chpdifbndlem1  26135  selberg3lem1  26139  selberg4  26143  pntsval2  26158  pntibndlem2  26173  pntlemr  26184  pntlemf  26187  pntlemo  26189  ostth2lem2  26216  ostth2lem3  26217  brbtwn2  26697  axsegconlem9  26717  axpasch  26733  axeuclidlem  26754  axcontlem2  26757  axcontlem4  26759  axcontlem7  26762  axcontlem8  26763  finsumvtxdg2ssteplem4  27336  ipasslem2  28613  minvecolem2  28656  pjhthlem1  29172  wrdt2ind  30633  ccfldsrarelvec  31086  circlemeth  31938  subfacval2  32461  subfaclim  32462  faclimlem1  33002  itgaddnc  35029  itgmulc2nc  35037  dvasin  35053  nnadddir  39345  nnmul1com  39346  nnmulcom  39347  resubdi  39408  sn-negex12  39427  sn-mul01  39435  sn-mulid2  39449  cu3addd  39477  3cubeslem3l  39483  3cubeslem3r  39484  pellexlem6  39631  pell1234qrmulcl  39652  rmxyadd  39718  jm2.25  39796  relexpmulnn  40266  binomcxplemnotnn0  40920  sumnnodd  42138  dvnmul  42451  stoweidlem13  42521  wallispilem4  42576  wallispi2lem1  42579  wallispi2lem2  42580  stirlinglem1  42582  stirlinglem6  42587  stirlinglem7  42588  stirlinglem8  42589  stirlinglem10  42591  dirkerper  42604  dirkertrigeqlem1  42606  dirkertrigeqlem2  42607  dirkertrigeqlem3  42608  fourierdlem83  42697  hoidmvlelem2  43101  hspmbllem1  43131  smfmullem1  43289  deccarry  43734  fmtnorec4  43932  mod42tp1mod8  43986  lighneallem3  43991  opoeALTV  44067  opeoALTV  44068  2zlidl  44424  2zrngamgm  44429  altgsumbcALT  44620  itcovalpclem2  44939  ackval2  44950  affinecomb2  44971  itscnhlc0yqe  45027  itsclc0yqsollem1  45030  itsclc0yqsol  45032  itscnhlc0xyqsol  45033  itsclc0xyqsolr  45037  itscnhlinecirc02plem1  45050
  Copyright terms: Public domain W3C validator