Theorem addassd 11259

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 11215	. 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 7417  ℂcc 11126   + caddc 11131

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

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

This theorem is used by:  addrid  11418  cnegex  11419  addlid  11421  addcan  11422  addcan2  11423  addcom  11424  addcomd  11440  muladd11r  11451  negeu  11475  addsubass  11495  nppcan3  11510  addsubsub23  11650  muladd  11674  nnadd1com  12287  nnaddcom  12288  nnadddir  12320  add1p1  12523  div4p1lem1div2  12527  zpnn0elfzo1  13799  flhalf  13895  fldiv  13925  binom3  14292  bernneq  14297  discr1  14307  ccatass  14658  cshweqrep  14896  01sqrexlem7  15339  sqreulem  15451  isercoll2  15760  caucvgrlem  15764  iseraltlem2  15774  bcxmas  15928  bpoly4  16151  efsep  16204  efi4p  16231  efival  16246  pwp1fsum  16487  flodddiv4  16511  sadadd2lem2  16546  sadadd2lem  16555  sadasslem  16566  pcadd2  16988  prmreclem6  17019  4sqlem11  17053  vdwapun  17072  vdwlem3  17081  vdwlem6  17084  vdwlem8  17086  vdwlem9  17087  prmgaplem8  17156  psgnunilem2  19628  sylow1lem1  19731  efgredlemc  19878  psdmul  22400  opnreen  25064  ovolunlem1a  25730  nulmbl2  25770  unmbl  25771  volinun  25780  uniioombllem5  25821  itgcnlem  26024  ditgsplit  26095  dvnadd  26163  dvntaylp  26614  ulmshft  26633  ulmcn  26642  tangtx  26750  heron  27083  quad2  27084  dcubic1lem  27088  mcubic  27092  binom4  27095  dquartlem1  27096  dquartlem2  27097  dquart  27098  quart1  27101  quart  27106  lgamcvg2  27299  basellem2  27326  basellem3  27327  basellem8  27332  ppiub  27448  bcp1ctr  27523  bposlem9  27536  2lgslem3c  27642  2lgslem3d  27643  selberg3  27803  pntpbnd2  27831  pntibndlem2  27835  pntlemg  27842  pntlemk  27850  pntlemo  27851  axeuclidlem  29427  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  finsumvtxdg2ssteplem4  30016  wwlksnextwrd  30373  wwlksnextproplem3  30387  wwlksext2clwwlk  30535  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  smcnlem  31186  stadd3i  32737  golem1  32760  quad3d  33228  cycpmco2lem3  33576  cycpmco2lem4  33577  cycpmco2lem5  33578  cycpmco2lem6  33579  cycpmco2  33581  archirngz  33637  constrrtlc1  34250  constrrtcclem  34252  constrrtcc  34253  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  subfacval2  35774  subfaclim  35775  subfacval3  35776  faclimlem1  36330  faclim2  36335  fwddifnp1  36753  dnizphlfeqhlf  37181  dnibndlem10  37192  dnibndlem13  37195  qdiff  38087  poimirlem16  38393  itg2addnclem3  38430  itg2addnc  38431  areacirclem1  38465  aks4d1p1p2  42944  posbezout  42974  2np3bcnp1  43018  sticksstones12a  43031  bcle2d  43053  aks6d1c7lem1  43054  quadfac  43079  readdridaddlidd  43132  resubeulem1  43258  resubeulem2  43259  readdsub  43267  resubsub4  43272  resubidaddlidlem  43277  sn-addlid  43287  renegneg  43295  readdcan2  43296  renegid2  43297  sn-it0e0  43299  sn-negex12  43300  sn-addcand  43303  sn-addrid  43304  sn-addcan2d  43305  sn-subeu  43310  sn-0tie0  43347  zaddcomlem  43359  zaddcom  43360  cnreeu  43386  dffltz  43488  3cubeslem2  43538  3cubeslem3l  43539  3cubeslem3r  43540  jm2.19lem3  43840  jm2.25  43848  int-addassocd  45022  binomcxplemnotnn0  45188  sub2times  46114  fperiodmullem  46144  dvnmul  46779  wallispilem4  46904  wallispi2lem2  46908  stirlinglem6  46915  dirkerper  46932  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  dirkercncflem1  46939  fourierdlem26  46969  fourierdlem35  46978  fourierdlem42  46985  fourierdlem51  46993  fourierdlem64  47006  fourierdlem111  47053  hoidmv1lelem2  47428  hoidmvlelem2  47432  smflimlem4  47610  deccarry  48207  sqrtpwpw2p  48449  fmtnorec2lem  48453  fmtnorec3  48459  fmtnorec4  48460  mod42tp1mod8  48513  gpg5nbgrvtx13starlem2  48996  itcovalpclem2  49609  ackval1  49619  ackval2  49620  itscnhlc0yqe  49697  itsclquadb  49714  sinhpcosh  50674  crosspdotsumlem  50805  crossp3d  50808  veroquadgsumlem  50824