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

Theorem addassd 9102
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 9069 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980    + caddc 8985
This theorem is referenced by:  addid1  9238  cnegex  9239  addid2  9241  addcan  9242  addcan2  9243  addcom  9244  addcomd  9260  negeu  9288  addsubass  9307  nppcan3  9317  muladd  9458  flhalf  11223  fldiv  11233  binom3  11492  bernneq  11497  discr1  11507  ccatass  11742  sqrlem7  12046  sqreulem  12155  isercoll2  12454  caucvgrlem  12458  iseraltlem2  12468  bcxmas  12607  efsep  12703  efi4p  12730  efival  12745  sadadd2lem2  12954  sadadd2lem  12963  sadasslem  12974  pcadd2  13251  prmreclem6  13281  4sqlem11  13315  vdwapun  13334  vdwlem3  13343  vdwlem6  13346  vdwlem8  13348  vdwlem9  13349  sylow1lem1  15224  efgredlemc  15369  opnreen  18854  ovolunlem1a  19384  nulmbl2  19423  unmbl  19424  volinun  19432  uniioombllem5  19471  itgcnlem  19673  ditgsplit  19740  dvnadd  19807  dvntaylp  20279  ulmshft  20298  ulmcn  20307  tangtx  20405  quad2  20671  dcubic1lem  20675  mcubic  20679  binom4  20682  dquartlem1  20683  dquartlem2  20684  dquart  20685  quart1  20688  quart  20693  basellem2  20856  basellem3  20857  basellem8  20862  ppiub  20980  bcp1ctr  21055  bposlem9  21068  selberg3  21245  pntpbnd2  21273  pntibndlem2  21277  pntlemg  21284  pntlemk  21292  pntlemo  21293  smcnlem  22185  stadd3i  23743  golem1  23766  lgamcvg2  24831  subfacval2  24865  subfaclim  24866  subfacval3  24867  relexpadd  25130  faclimlem1  25354  faclim2  25359  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  bpoly4  26097  itg2addnclem3  26248  itg2addnc  26249  areacirclem2  26282  jm2.19lem3  27053  jm2.25  27061  psgnunilem2  27386  wallispilem4  27784  wallispi2lem2  27788  stirlinglem6  27795  cshweqrep  28237  sinhpcosh  28420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 9047
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator