Theorem addassd 11312

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 11268	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   + caddc 11184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11246

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11471  cnegex  11472  addlid  11474  addcan  11475  addcan2  11476  addcom  11477  addcomd  11493  muladd11r  11504  negeu  11528  addsubass  11548  nppcan3  11563  addsubsub23  11703  muladd  11729  nnadd1com  12342  nnaddcom  12343  nnadddir  12375  add1p1  12578  div4p1lem1div2  12582  zpnn0elfzo1  13854  flhalf  13950  fldiv  13980  binom3  14348  bernneq  14353  discr1  14363  ccatass  14714  cshweqrep  14952  01sqrexlem7  15395  sqreulem  15507  isercoll2  15816  caucvgrlem  15820  iseraltlem2  15830  bcxmas  15984  bpoly4  16205  efsep  16258  efi4p  16285  efival  16300  pwp1fsum  16541  flodddiv4  16565  sadadd2lem2  16600  sadadd2lem  16609  sadasslem  16620  pcadd2  17048  prmreclem6  17079  4sqlem11  17113  vdwapun  17132  vdwlem3  17141  vdwlem6  17144  vdwlem8  17146  vdwlem9  17147  prmgaplem8  17216  psgnunilem2  19689  sylow1lem1  19792  efgredlemc  19939  psdmul  22467  opnreen  25131  ovolunlem1a  25797  nulmbl2  25837  unmbl  25838  volinun  25847  uniioombllem5  25888  itgcnlem  26090  ditgsplit  26161  dvnadd  26229  dvntaylp  26680  ulmshft  26699  ulmcn  26708  tangtx  26816  heron  27148  quad2  27149  dcubic1lem  27153  mcubic  27157  binom4  27160  dquartlem1  27161  dquartlem2  27162  dquart  27163  quart1  27166  quart  27171  lgamcvg2  27364  basellem2  27391  basellem3  27392  basellem8  27397  ppiub  27513  bcp1ctr  27588  bposlem9  27601  2lgslem3c  27707  2lgslem3d  27708  selberg3  27868  pntpbnd2  27896  pntibndlem2  27900  pntlemg  27907  pntlemk  27915  pntlemo  27916  axeuclidlem  29522  axcontlem2  29525  axcontlem4  29527  axcontlem7  29530  finsumvtxdg2ssteplem4  30111  wwlksnextwrd  30468  wwlksnextproplem3  30482  wwlksext2clwwlk  30630  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  smcnlem  31281  stadd3i  32832  golem1  32855  quad3d  33323  cycpmco2lem3  33671  cycpmco2lem4  33672  cycpmco2lem5  33673  cycpmco2lem6  33674  cycpmco2  33676  archirngz  33732  constrrtlc1  34346  constrrtcclem  34348  constrrtcc  34349  cos9thpiminplylem1  34396  cos9thpiminplylem2  34397  subfacval2  35921  subfaclim  35922  subfacval3  35923  faclimlem1  36477  faclim2  36482  fwddifnp1  36900  dnizphlfeqhlf  37312  dnibndlem10  37323  dnibndlem13  37326  qdiff  38216  poimirlem16  38522  itg2addnclem3  38559  itg2addnc  38560  areacirclem1  38594  aks4d1p1p2  43088  posbezout  43118  2np3bcnp1  43162  sticksstones12a  43175  bcle2d  43197  aks6d1c7lem1  43198  quadfac  43223  readdridaddlidd  43276  resubeulem1  43394  resubeulem2  43395  readdsub  43403  resubsub4  43408  resubidaddlidlem  43413  sn-addlid  43423  renegneg  43431  readdcan2  43432  renegid2  43433  sn-it0e0  43435  sn-negex12  43436  sn-addcand  43439  sn-addrid  43440  sn-addcan2d  43441  sn-subeu  43446  sn-0tie0  43483  zaddcomlem  43495  zaddcom  43496  cnreeu  43522  dffltz  43624  3cubeslem2  43649  3cubeslem3l  43650  3cubeslem3r  43651  jm2.19lem3  43951  jm2.25  43959  int-addassocd  45133  binomcxplemnotnn0  45299  sub2times  46232  fperiodmullem  46262  dvnmul  46897  wallispilem4  47022  wallispi2lem2  47026  stirlinglem6  47033  dirkerper  47050  dirkertrigeqlem1  47052  dirkertrigeqlem2  47053  dirkertrigeqlem3  47054  dirkercncflem1  47057  fourierdlem26  47087  fourierdlem35  47096  fourierdlem42  47103  fourierdlem51  47111  fourierdlem64  47124  fourierdlem111  47171  hoidmv1lelem2  47546  hoidmvlelem2  47550  smflimlem4  47728  deccarry  48325  sqrtpwpw2p  48567  fmtnorec2lem  48571  fmtnorec3  48577  fmtnorec4  48578  mod42tp1mod8  48631  gpg5nbgrvtx13starlem2  49114  itcovalpclem2  49727  ackval1  49737  ackval2  49738  itscnhlc0yqe  49815  itsclquadb  49832  sinhpcosh  50777  crosspdotsumlem  50908  crossp3d  50911  veroquadgsumlem  50927