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

Theorem addassd 8873
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 8840 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  addid1  9008  cnegex  9009  addid2  9011  addcan  9012  addcan2  9013  addcom  9014  addcomd  9030  negeu  9058  addsubass  9077  nppcan3  9087  muladd  9228  flhalf  10970  fldiv  10980  binom3  11238  bernneq  11243  discr1  11253  ccatass  11452  sqrlem7  11750  sqreulem  11859  isercoll2  12158  caucvgrlem  12161  iseraltlem2  12171  bcxmas  12310  efsep  12406  efi4p  12433  efival  12448  sadadd2lem2  12657  sadadd2lem  12666  sadasslem  12677  pcadd2  12954  prmreclem6  12984  4sqlem11  13018  vdwapun  13037  vdwlem3  13046  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  sylow1lem1  14925  efgredlemc  15070  opnreen  18352  ovolunlem1a  18871  nulmbl2  18910  unmbl  18911  volinun  18919  uniioombllem5  18958  itgcnlem  19160  ditgsplit  19227  dvnadd  19294  dvntaylp  19766  ulmshft  19785  ulmcn  19792  tangtx  19889  quad2  20151  dcubic1lem  20155  mcubic  20159  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1  20168  quart  20173  basellem2  20335  basellem3  20336  basellem8  20341  ppiub  20459  bcp1ctr  20534  bposlem9  20547  selberg3  20724  pntpbnd2  20752  pntibndlem2  20756  pntlemg  20763  pntlemk  20771  pntlemo  20772  smcnlem  21286  stadd3i  22844  golem1  22867  subfacval2  23733  subfaclim  23734  subfacval3  23735  relexpadd  24050  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  bpoly4  24866  itg2addnc  25005  itgaddnclem2  25010  areacirclem2  25028  addassv  25759  jm2.19lem3  27187  jm2.25  27195  psgnunilem2  27521  wallispilem4  27920  wallispi2lem2  27924  stirlinglem6  27931  sinhpcosh  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 8818
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator