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

Theorem addassd 9411
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 9372 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1218 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6094   CCcc 9283    + caddc 9288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9350
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  addid1  9552  cnegex  9553  addid2  9555  addcan  9556  addcan2  9557  addcom  9558  addcomd  9574  negeu  9603  addsubass  9623  nppcan3  9636  muladd  9780  flhalf  11677  fldiv  11702  binom3  11988  bernneq  11993  discr1  12003  ccatass  12289  cshweqrep  12458  sqrlem7  12741  sqreulem  12850  isercoll2  13149  caucvgrlem  13153  iseraltlem2  13163  bcxmas  13301  efsep  13397  efi4p  13424  efival  13439  sadadd2lem2  13649  sadadd2lem  13658  sadasslem  13669  pcadd2  13955  prmreclem6  13985  4sqlem11  14019  vdwapun  14038  vdwlem3  14047  vdwlem6  14050  vdwlem8  14052  vdwlem9  14053  psgnunilem2  16004  sylow1lem1  16100  efgredlemc  16245  opnreen  20411  ovolunlem1a  20982  nulmbl2  21021  unmbl  21022  volinun  21030  uniioombllem5  21070  itgcnlem  21270  ditgsplit  21339  dvnadd  21406  dvntaylp  21839  ulmshft  21858  ulmcn  21867  tangtx  21970  heron  22236  quad2  22237  dcubic1lem  22241  mcubic  22245  binom4  22248  dquartlem1  22249  dquartlem2  22250  dquart  22251  quart1  22254  quart  22259  basellem2  22422  basellem3  22423  basellem8  22428  ppiub  22546  bcp1ctr  22621  bposlem9  22634  selberg3  22811  pntpbnd2  22839  pntibndlem2  22843  pntlemg  22850  pntlemk  22858  pntlemo  22859  axeuclidlem  23211  axcontlem2  23214  axcontlem4  23216  axcontlem7  23219  smcnlem  24095  stadd3i  25655  golem1  25678  archirngz  26209  lgamcvg2  27044  subfacval2  27078  subfaclim  27079  subfacval3  27080  relexpadd  27343  faclimlem1  27552  faclim2  27557  bpoly4  28205  itg2addnclem3  28448  itg2addnc  28449  areacirclem1  28487  jm2.19lem3  29343  jm2.25  29351  wallispilem4  29866  wallispi2lem2  29870  stirlinglem6  29877  add1p1  30183  zpnn0elfzo1  30225  wwlkextwrd  30363  wwlkext2clwwlk  30468  wwlkextproplem3  30565  numclwlk1lem2fo  30691  numclwlk2lem2f  30699  numclwlk2lem2f1o  30701  sinhpcosh  31078
  Copyright terms: Public domain W3C validator