Theorem addassd 10062

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

Step	Hyp	Ref	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 10023	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
5	1, 2, 3, 4	syl3anc 1326	1 |- ( ph -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10001

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  addid1  10216  cnegex  10217  addid2  10219  addcan  10220  addcan2  10221  addcom  10222  addcomd  10238  muladd11r  10249  negeu  10271  addsubass  10291  nppcan3  10305  muladd  10462  add1p1  11283  div4p1lem1div2  11287  zpnn0elfzo1  12541  flhalf  12631  fldiv  12659  binom3  12985  bernneq  12990  discr1  13000  ccatass  13371  cshweqrep  13567  sqrlem7  13989  sqreulem  14099  isercoll2  14399  caucvgrlem  14403  iseraltlem2  14413  bcxmas  14567  bpoly4  14790  efsep  14840  efi4p  14867  efival  14882  pwp1fsum  15114  flodddiv4  15137  sadadd2lem2  15172  sadadd2lem  15181  sadasslem  15192  pcadd2  15594  prmreclem6  15625  4sqlem11  15659  vdwapun  15678  vdwlem3  15687  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  prmgaplem8  15762  psgnunilem2  17915  sylow1lem1  18013  efgredlemc  18158  opnreen  22634  ovolunlem1a  23264  nulmbl2  23304  unmbl  23305  volinun  23314  uniioombllem5  23355  itgcnlem  23556  ditgsplit  23625  dvnadd  23692  dvntaylp  24125  ulmshft  24144  ulmcn  24153  tangtx  24257  heron  24565  quad2  24566  dcubic1lem  24570  mcubic  24574  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1  24583  quart  24588  lgamcvg2  24781  basellem2  24808  basellem3  24809  basellem8  24814  ppiub  24929  bcp1ctr  25004  bposlem9  25017  2lgslem3c  25123  2lgslem3d  25124  selberg3  25248  pntpbnd2  25276  pntibndlem2  25280  pntlemg  25287  pntlemk  25295  pntlemo  25296  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  finsumvtxdg2ssteplem4  26444  wwlksnextwrd  26792  wwlksnextproplem3  26806  wwlksext2clwwlk  26924  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  smcnlem  27552  stadd3i  29107  golem1  29130  archirngz  29743  subfacval2  31169  subfaclim  31170  subfacval3  31171  faclimlem1  31629  faclim2  31634  fwddifnp1  32272  dnizphlfeqhlf  32466  dnibndlem10  32477  dnibndlem13  32480  poimirlem16  33425  itg2addnclem3  33463  itg2addnc  33464  areacirclem1  33500  jm2.19lem3  37558  jm2.25  37566  int-addassocd  38477  binomcxplemnotnn0  38555  sub2times  39485  fperiodmullem  39517  dvnmul  40158  wallispilem4  40285  wallispi2lem2  40289  stirlinglem6  40296  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkercncflem1  40320  fourierdlem26  40350  fourierdlem35  40359  fourierdlem42  40366  fourierdlem51  40374  fourierdlem64  40387  fourierdlem111  40434  hoidmv1lelem2  40806  hoidmvlelem2  40810  smflimlem4  40982  deccarry  41321  sqrtpwpw2p  41450  fmtnorec2lem  41454  fmtnorec3  41460  fmtnorec4  41461  mod42tp1mod8  41519  sinhpcosh  42481