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

Theorem addassd 8857
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 8824 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  addid1  8992  cnegex  8993  addid2  8995  addcan  8996  addcan2  8997  addcom  8998  addcomd  9014  negeu  9042  addsubass  9061  nppcan3  9071  muladd  9212  flhalf  10954  fldiv  10964  binom3  11222  bernneq  11227  discr1  11237  ccatass  11436  sqrlem7  11734  sqreulem  11843  isercoll2  12142  caucvgrlem  12145  iseraltlem2  12155  bcxmas  12294  efsep  12390  efi4p  12417  efival  12432  sadadd2lem2  12641  sadadd2lem  12650  sadasslem  12661  pcadd2  12938  prmreclem6  12968  4sqlem11  13002  vdwapun  13021  vdwlem3  13030  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  sylow1lem1  14909  efgredlemc  15054  opnreen  18336  ovolunlem1a  18855  nulmbl2  18894  unmbl  18895  volinun  18903  uniioombllem5  18942  itgcnlem  19144  ditgsplit  19211  dvnadd  19278  dvntaylp  19750  ulmshft  19769  ulmcn  19776  tangtx  19873  quad2  20135  dcubic1lem  20139  mcubic  20143  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1  20152  quart  20157  basellem2  20319  basellem3  20320  basellem8  20325  ppiub  20443  bcp1ctr  20518  bposlem9  20531  selberg3  20708  pntpbnd2  20736  pntibndlem2  20740  pntlemg  20747  pntlemk  20755  pntlemo  20756  smcnlem  21270  stadd3i  22828  golem1  22851  subfacval2  23718  subfaclim  23719  subfacval3  23720  relexpadd  24035  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  bpoly4  24794  areacirclem2  24925  addassv  25656  jm2.19lem3  27084  jm2.25  27092  psgnunilem2  27418  wallispilem4  27817  wallispi2lem2  27821  stirlinglem6  27828  sinhpcosh  28210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 8802
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator