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

Theorem addassd 9043
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 9010 . 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 1649    e. wcel 1717  (class class class)co 6020   CCcc 8921    + caddc 8926
This theorem is referenced by:  addid1  9178  cnegex  9179  addid2  9181  addcan  9182  addcan2  9183  addcom  9184  addcomd  9200  negeu  9228  addsubass  9247  nppcan3  9257  muladd  9398  flhalf  11158  fldiv  11168  binom3  11427  bernneq  11432  discr1  11442  ccatass  11677  sqrlem7  11981  sqreulem  12090  isercoll2  12389  caucvgrlem  12393  iseraltlem2  12403  bcxmas  12542  efsep  12638  efi4p  12665  efival  12680  sadadd2lem2  12889  sadadd2lem  12898  sadasslem  12909  pcadd2  13186  prmreclem6  13216  4sqlem11  13250  vdwapun  13269  vdwlem3  13278  vdwlem6  13281  vdwlem8  13283  vdwlem9  13284  sylow1lem1  15159  efgredlemc  15304  opnreen  18733  ovolunlem1a  19259  nulmbl2  19298  unmbl  19299  volinun  19307  uniioombllem5  19346  itgcnlem  19548  ditgsplit  19615  dvnadd  19682  dvntaylp  20154  ulmshft  20173  ulmcn  20182  tangtx  20280  quad2  20546  dcubic1lem  20550  mcubic  20554  binom4  20557  dquartlem1  20558  dquartlem2  20559  dquart  20560  quart1  20563  quart  20568  basellem2  20731  basellem3  20732  basellem8  20737  ppiub  20855  bcp1ctr  20930  bposlem9  20943  selberg3  21120  pntpbnd2  21148  pntibndlem2  21152  pntlemg  21159  pntlemk  21167  pntlemo  21168  smcnlem  22041  stadd3i  23599  golem1  23622  lgamcvg2  24618  subfacval2  24652  subfaclim  24653  subfacval3  24654  relexpadd  24917  faclimlem1  25120  faclim2  25125  axeuclidlem  25615  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  bpoly4  25819  itg2addnc  25959  itgaddnclem2  25964  areacirclem2  25982  jm2.19lem3  26753  jm2.25  26761  psgnunilem2  27087  wallispilem4  27485  wallispi2lem2  27489  stirlinglem6  27496  sinhpcosh  27829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 8988
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator