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

Theorem adddid 9609
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
adddid  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Proof of Theorem adddid
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 adddi 9570 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1226 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479    + caddc 9484    x. cmul 9486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9548
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  addid1  9749  cnegex  9750  addcom  9755  addcomd  9771  subdi  9986  conjmul  10257  cju  10527  flhalf  11944  modcyc  12014  binom3  12272  bcpasc  12384  hashf1lem2  12492  remim  13035  mulre  13039  readd  13044  remullem  13046  imadd  13052  cjadd  13059  sqreulem  13277  iseraltlem2  13590  o1fsum  13712  binomlem  13726  climcndslem2  13747  tanval3  13954  sinadd  13984  tanadd  13987  dvdsmulgcd  14279  pythagtriplem1  14427  pcaddlem  14494  prmreclem4  14524  prmreclem6  14526  mul4sqlem  14558  vdwlem3  14588  vdwlem6  14591  vdwlem9  14594  nn0srg  18684  rge0srg  18685  icopnfcnv  21611  pcoass  21693  minveclem2  22010  pjthlem1  22021  ovolunlem1a  22076  ovolscalem1  22093  itgcnlem  22365  itgadd  22400  itgmulc2  22409  itgsplit  22411  aaliou3lem2  22908  abelthlem7  23002  tangtx  23067  efgh  23097  tanarg  23175  logcnlem4  23197  mulcxp  23237  cxpmul2  23241  heron  23369  quad2  23370  dcubic1lem  23374  dcubic2  23375  mcubic  23378  binom4  23381  quart1  23387  atanlogsublem  23446  2efiatan  23449  basellem2  23556  basellem3  23557  basellem8  23562  chtub  23688  bposlem9  23768  lgseisenlem2  23826  2sqlem4  23843  2sqlem8  23848  dchrisumlem1  23875  dchrvmasum2if  23883  dchrisum0re  23899  mulog2sumlem1  23920  selberglem1  23931  selberglem2  23932  selberg  23934  selberg2  23937  chpdifbndlem1  23939  selberg3lem1  23943  selberg4  23947  pntsval2  23962  pntibndlem2  23977  pntlemr  23988  pntlemf  23991  pntlemo  23993  ostth2lem2  24020  ostth2lem3  24021  brbtwn2  24413  axsegconlem9  24433  axpasch  24449  axeuclidlem  24470  axcontlem2  24473  axcontlem4  24475  axcontlem7  24478  axcontlem8  24479  ipasslem2  25948  minvecolem2  25992  pjhthlem1  26510  lgamgulmlem3  28840  subfacval2  28898  subfaclim  28899  binomfallfaclem2  29406  faclimlem1  29412  bpoly4  30052  itgaddnc  30318  itgmulc2nc  30326  dvasin  30346  pellexlem6  31012  pell1234qrmulcl  31033  rmxyadd  31099  jm2.25  31183  lcmgcdlem  31456  binomcxplemnotnn0  31505  m1expeven  31827  sumnnodd  31878  dvnmul  31982  stoweidlem13  32037  wallispilem4  32092  wallispi2lem1  32095  wallispi2lem2  32096  stirlinglem1  32098  stirlinglem6  32103  stirlinglem7  32104  stirlinglem8  32105  stirlinglem10  32107  dirkerper  32120  dirkertrigeqlem1  32122  dirkertrigeqlem2  32123  dirkertrigeqlem3  32124  fourierdlem83  32214  opoeALTV  32597  opeoALTV  32598  2zlidl  33013  2zrngamgm  33018  altgsumbcALT  33215  relexpmulnn  38248
  Copyright terms: Public domain W3C validator