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

Theorem addassd 9400
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 9361 . 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 6086   CCcc 9272    + caddc 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9339
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  addid1  9541  cnegex  9542  addid2  9544  addcan  9545  addcan2  9546  addcom  9547  addcomd  9563  negeu  9592  addsubass  9612  nppcan3  9625  muladd  9769  flhalf  11666  fldiv  11691  binom3  11977  bernneq  11982  discr1  11992  ccatass  12278  cshweqrep  12447  sqrlem7  12730  sqreulem  12839  isercoll2  13138  caucvgrlem  13142  iseraltlem2  13152  bcxmas  13290  efsep  13386  efi4p  13413  efival  13428  sadadd2lem2  13638  sadadd2lem  13647  sadasslem  13658  pcadd2  13944  prmreclem6  13974  4sqlem11  14008  vdwapun  14027  vdwlem3  14036  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  psgnunilem2  15990  sylow1lem1  16086  efgredlemc  16231  opnreen  20377  ovolunlem1a  20948  nulmbl2  20987  unmbl  20988  volinun  20996  uniioombllem5  21036  itgcnlem  21236  ditgsplit  21305  dvnadd  21372  dvntaylp  21805  ulmshft  21824  ulmcn  21833  tangtx  21936  heron  22202  quad2  22203  dcubic1lem  22207  mcubic  22211  binom4  22214  dquartlem1  22215  dquartlem2  22216  dquart  22217  quart1  22220  quart  22225  basellem2  22388  basellem3  22389  basellem8  22394  ppiub  22512  bcp1ctr  22587  bposlem9  22600  selberg3  22777  pntpbnd2  22805  pntibndlem2  22809  pntlemg  22816  pntlemk  22824  pntlemo  22825  axeuclidlem  23153  axcontlem2  23156  axcontlem4  23158  axcontlem7  23161  smcnlem  24037  stadd3i  25597  golem1  25620  archirngz  26151  lgamcvg2  26989  subfacval2  27023  subfaclim  27024  subfacval3  27025  relexpadd  27287  faclimlem1  27496  faclim2  27501  bpoly4  28149  itg2addnclem3  28388  itg2addnc  28389  areacirclem1  28427  jm2.19lem3  29283  jm2.25  29291  wallispilem4  29806  wallispi2lem2  29810  stirlinglem6  29817  add1p1  30123  zpnn0elfzo1  30165  wwlkextwrd  30303  wwlkext2clwwlk  30408  wwlkextproplem3  30505  numclwlk1lem2fo  30631  numclwlk2lem2f  30639  numclwlk2lem2f1o  30641  sinhpcosh  30934
  Copyright terms: Public domain W3C validator