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 1223 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762  (class class class)co 6275   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 371  df-3an 970
This theorem is referenced by:  addid1  9748  cnegex  9749  addid2  9751  addcan  9752  addcan2  9753  addcom  9754  addcomd  9770  negeu  9799  addsubass  9819  nppcan3  9832  muladd  9978  add1p1  10777  zpnn0elfzo1  11846  flhalf  11918  fldiv  11943  binom3  12242  bernneq  12247  discr1  12257  ccatass  12557  cshweqrep  12739  sqrlem7  13032  sqreulem  13141  isercoll2  13440  caucvgrlem  13444  iseraltlem2  13454  bcxmas  13599  efsep  13695  efi4p  13722  efival  13737  sadadd2lem2  13948  sadadd2lem  13957  sadasslem  13968  pcadd2  14257  prmreclem6  14287  4sqlem11  14321  vdwapun  14340  vdwlem3  14349  vdwlem6  14352  vdwlem8  14354  vdwlem9  14355  psgnunilem2  16309  sylow1lem1  16407  efgredlemc  16552  opnreen  21064  ovolunlem1a  21635  nulmbl2  21675  unmbl  21676  volinun  21684  uniioombllem5  21724  itgcnlem  21924  ditgsplit  21993  dvnadd  22060  dvntaylp  22493  ulmshft  22512  ulmcn  22521  tangtx  22624  heron  22890  quad2  22891  dcubic1lem  22895  mcubic  22899  binom4  22902  dquartlem1  22903  dquartlem2  22904  dquart  22905  quart1  22908  quart  22913  basellem2  23076  basellem3  23077  basellem8  23082  ppiub  23200  bcp1ctr  23275  bposlem9  23288  selberg3  23465  pntpbnd2  23493  pntibndlem2  23497  pntlemg  23504  pntlemk  23512  pntlemo  23513  axeuclidlem  23934  axcontlem2  23937  axcontlem4  23939  axcontlem7  23942  wwlkextwrd  24390  wwlkextproplem3  24405  wwlkext2clwwlk  24465  numclwlk1lem2fo  24758  numclwlk2lem2f  24766  numclwlk2lem2f1o  24768  smcnlem  25269  stadd3i  26829  golem1  26852  archirngz  27381  lgamcvg2  28223  subfacval2  28257  subfaclim  28258  subfacval3  28259  relexpadd  28522  faclimlem1  28731  faclim2  28736  bpoly4  29384  itg2addnclem3  29632  itg2addnc  29633  areacirclem1  29671  jm2.19lem3  30526  jm2.25  30534  sub2times  30987  fperiodmullem  31035  wallispilem4  31323  wallispi2lem2  31327  stirlinglem6  31334  dirkerper  31351  dirkertrigeqlem1  31353  dirkertrigeqlem2  31354  dirkertrigeqlem3  31355  dirkercncflem1  31358  fourierdlem26  31388  fourierdlem35  31397  fourierdlem42  31404  fourierdlem51  31413  fourierdlem64  31426  fourierdlem65  31427  fourierdlem111  31473  sinhpcosh  32090
  Copyright terms: Public domain W3C validator