Theorem addassd 11240

Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
addassd	⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		addass 11199	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	syl3anc 1371	1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110   + caddc 11115

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089

This theorem is referenced by:  addrid  11398  cnegex  11399  addlid  11401  addcan  11402  addcan2  11403  addcom  11404  addcomd  11420  muladd11r  11431  negeu  11454  addsubass  11474  nppcan3  11488  muladd  11650  add1p1  12467  div4p1lem1div2  12471  zpnn0elfzo1  13710  flhalf  13799  fldiv  13829  binom3  14191  bernneq  14196  discr1  14206  ccatass  14542  cshweqrep  14775  01sqrexlem7  15199  sqreulem  15310  isercoll2  15619  caucvgrlem  15623  iseraltlem2  15633  bcxmas  15785  bpoly4  16007  efsep  16057  efi4p  16084  efival  16099  pwp1fsum  16338  flodddiv4  16360  sadadd2lem2  16395  sadadd2lem  16404  sadasslem  16415  pcadd2  16827  prmreclem6  16858  4sqlem11  16892  vdwapun  16911  vdwlem3  16920  vdwlem6  16923  vdwlem8  16925  vdwlem9  16926  prmgaplem8  16995  psgnunilem2  19404  sylow1lem1  19507  efgredlemc  19654  opnreen  24567  ovolunlem1a  25237  nulmbl2  25277  unmbl  25278  volinun  25287  uniioombllem5  25328  itgcnlem  25531  ditgsplit  25602  dvnadd  25670  dvntaylp  26107  ulmshft  26126  ulmcn  26135  tangtx  26239  heron  26567  quad2  26568  dcubic1lem  26572  mcubic  26576  binom4  26579  dquartlem1  26580  dquartlem2  26581  dquart  26582  quart1  26585  quart  26590  lgamcvg2  26783  basellem2  26810  basellem3  26811  basellem8  26816  ppiub  26931  bcp1ctr  27006  bposlem9  27019  2lgslem3c  27125  2lgslem3d  27126  selberg3  27286  pntpbnd2  27314  pntibndlem2  27318  pntlemg  27325  pntlemk  27333  pntlemo  27334  axeuclidlem  28475  axcontlem2  28478  axcontlem4  28480  axcontlem7  28483  finsumvtxdg2ssteplem4  29060  wwlksnextwrd  29406  wwlksnextproplem3  29420  wwlksext2clwwlk  29565  numclwlk2lem2f  29885  numclwlk2lem2f1o  29887  smcnlem  30205  stadd3i  31756  golem1  31779  cycpmco2lem3  32545  cycpmco2lem4  32546  cycpmco2lem5  32547  cycpmco2lem6  32548  cycpmco2  32550  archirngz  32593  subfacval2  34464  subfaclim  34465  subfacval3  34466  faclimlem1  35005  faclim2  35010  fwddifnp1  35429  dnizphlfeqhlf  35655  dnibndlem10  35666  dnibndlem13  35669  poimirlem16  36807  itg2addnclem3  36844  itg2addnc  36845  areacirclem1  36879  aks4d1p1p2  41241  2np3bcnp1  41266  sticksstones12a  41279  2xp3dxp2ge1d  41328  readdridaddlidd  41480  nnadd1com  41483  nnaddcom  41484  nnadddir  41486  resubeulem1  41550  resubeulem2  41551  readdsub  41559  resubsub4  41564  resubidaddlidlem  41569  sn-addlid  41579  renegneg  41586  readdcan2  41587  renegid2  41588  sn-it0e0  41590  sn-negex12  41591  sn-addcand  41594  sn-addrid  41595  sn-addcan2d  41596  sn-subeu  41601  sn-0tie0  41614  zaddcomlem  41626  zaddcom  41627  cnreeu  41643  dffltz  41678  3cubeslem2  41725  3cubeslem3l  41726  3cubeslem3r  41727  jm2.19lem3  42032  jm2.25  42040  int-addassocd  43228  binomcxplemnotnn0  43417  sub2times  44281  fperiodmullem  44312  dvnmul  44958  wallispilem4  45083  wallispi2lem2  45087  stirlinglem6  45094  dirkerper  45111  dirkertrigeqlem1  45113  dirkertrigeqlem2  45114  dirkertrigeqlem3  45115  dirkercncflem1  45118  fourierdlem26  45148  fourierdlem35  45157  fourierdlem42  45164  fourierdlem51  45172  fourierdlem64  45185  fourierdlem111  45232  hoidmv1lelem2  45607  hoidmvlelem2  45611  smflimlem4  45789  deccarry  46318  sqrtpwpw2p  46505  fmtnorec2lem  46509  fmtnorec3  46515  fmtnorec4  46516  mod42tp1mod8  46569  itcovalpclem2  47445  ackval1  47455  ackval2  47456  itscnhlc0yqe  47533  itsclquadb  47550  sinhpcosh  47873