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

Theorem addassd 9607
Description: Associative law for addition. (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
addassd  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )

Proof of Theorem addassd
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 addass 9568 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1226 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  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
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9546
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  addid1  9749  cnegex  9750  addid2  9752  addcan  9753  addcan2  9754  addcom  9755  addcomd  9771  negeu  9801  addsubass  9821  nppcan3  9834  muladd  9985  add1p1  10784  zpnn0elfzo1  11870  flhalf  11944  fldiv  11969  binom3  12269  bernneq  12274  discr1  12284  ccatass  12594  cshweqrep  12780  sqrlem7  13164  sqreulem  13274  isercoll2  13573  caucvgrlem  13577  iseraltlem2  13587  bcxmas  13729  efsep  13927  efi4p  13954  efival  13969  sadadd2lem2  14184  sadadd2lem  14193  sadasslem  14204  pcadd2  14493  prmreclem6  14523  4sqlem11  14557  vdwapun  14576  vdwlem3  14585  vdwlem6  14588  vdwlem8  14590  vdwlem9  14591  psgnunilem2  16719  sylow1lem1  16817  efgredlemc  16962  opnreen  21502  ovolunlem1a  22073  nulmbl2  22113  unmbl  22114  volinun  22122  uniioombllem5  22162  itgcnlem  22362  ditgsplit  22431  dvnadd  22498  dvntaylp  22932  ulmshft  22951  ulmcn  22960  tangtx  23064  heron  23366  quad2  23367  dcubic1lem  23371  mcubic  23375  binom4  23378  dquartlem1  23379  dquartlem2  23380  dquart  23381  quart1  23384  quart  23389  basellem2  23553  basellem3  23554  basellem8  23559  ppiub  23677  bcp1ctr  23752  bposlem9  23765  selberg3  23942  pntpbnd2  23970  pntibndlem2  23974  pntlemg  23981  pntlemk  23989  pntlemo  23990  axeuclidlem  24467  axcontlem2  24470  axcontlem4  24472  axcontlem7  24475  wwlkextwrd  24930  wwlkextproplem3  24945  wwlkext2clwwlk  25005  numclwlk1lem2fo  25297  numclwlk2lem2f  25305  numclwlk2lem2f1o  25307  smcnlem  25805  stadd3i  27365  golem1  27388  archirngz  27967  lgamcvg2  28861  subfacval2  28895  subfaclim  28896  subfacval3  28897  faclimlem1  29409  faclim2  29414  bpoly4  30049  itg2addnclem3  30308  itg2addnc  30309  areacirclem1  30347  jm2.19lem3  31172  jm2.25  31180  binomcxplemnotnn0  31502  sub2times  31695  fperiodmullem  31742  dvnmul  31979  wallispilem4  32089  wallispi2lem2  32093  stirlinglem6  32100  dirkerper  32117  dirkertrigeqlem1  32119  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkercncflem1  32124  fourierdlem26  32154  fourierdlem35  32163  fourierdlem42  32170  fourierdlem51  32179  fourierdlem64  32192  fourierdlem111  32239  sinhpcosh  33524  int-addassocd  38447
  Copyright terms: Public domain W3C validator