Theorem addassd 11201

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   + caddc 11073

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  addrid  11360  cnegex  11361  addlid  11363  addcan  11364  addcan2  11365  addcom  11366  addcomd  11382  muladd11r  11393  negeu  11417  addsubass  11437  nppcan3  11452  addsubsub23  11592  muladd  11616  nnadd1com  12233  nnaddcom  12234  nnadddir  12266  add1p1  12469  div4p1lem1div2  12473  zpnn0elfzo1  13742  flhalf  13837  fldiv  13867  binom3  14234  bernneq  14239  discr1  14249  ccatass  14599  cshweqrep  14831  01sqrexlem7  15258  sqreulem  15370  isercoll2  15679  caucvgrlem  15683  iseraltlem2  15693  bcxmas  15848  bpoly4  16072  efsep  16125  efi4p  16152  efival  16167  pwp1fsum  16408  flodddiv4  16432  sadadd2lem2  16467  sadadd2lem  16476  sadasslem  16487  pcadd2  16909  prmreclem6  16940  4sqlem11  16974  vdwapun  16993  vdwlem3  17002  vdwlem6  17005  vdwlem8  17007  vdwlem9  17008  prmgaplem8  17077  psgnunilem2  19518  sylow1lem1  19621  efgredlemc  19768  psdmul  22211  opnreen  24872  ovolunlem1a  25538  nulmbl2  25578  unmbl  25579  volinun  25588  uniioombllem5  25629  itgcnlem  25832  ditgsplit  25903  dvnadd  25971  dvntaylp  26411  ulmshft  26430  ulmcn  26439  tangtx  26547  heron  26880  quad2  26881  dcubic1lem  26885  mcubic  26889  binom4  26892  dquartlem1  26893  dquartlem2  26894  dquart  26895  quart1  26898  quart  26903  lgamcvg2  27096  basellem2  27123  basellem3  27124  basellem8  27129  ppiub  27245  bcp1ctr  27320  bposlem9  27333  2lgslem3c  27439  2lgslem3d  27440  selberg3  27600  pntpbnd2  27628  pntibndlem2  27632  pntlemg  27639  pntlemk  27647  pntlemo  27648  axeuclidlem  29109  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  finsumvtxdg2ssteplem4  29695  wwlksnextwrd  30043  wwlksnextproplem3  30057  wwlksext2clwwlk  30205  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  smcnlem  30846  stadd3i  32397  golem1  32420  quad3d  32901  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2  33274  archirngz  33330  constrrtlc1  33990  constrrtcclem  33992  constrrtcc  33993  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  subfacval2  35501  subfaclim  35502  subfacval3  35503  faclimlem1  36057  faclim2  36062  fwddifnp1  36479  dnizphlfeqhlf  36878  dnibndlem10  36889  dnibndlem13  36892  qdiff  37783  poimirlem16  38099  itg2addnclem3  38136  itg2addnc  38137  areacirclem1  38171  aks4d1p1p2  42651  posbezout  42681  2np3bcnp1  42725  sticksstones12a  42738  bcle2d  42760  aks6d1c7lem1  42761  readdridaddlidd  42837  resubeulem1  42948  resubeulem2  42949  readdsub  42957  resubsub4  42962  resubidaddlidlem  42967  sn-addlid  42977  renegneg  42985  readdcan2  42986  renegid2  42987  sn-it0e0  42989  sn-negex12  42990  sn-addcand  42993  sn-addrid  42994  sn-addcan2d  42995  sn-subeu  43000  sn-0tie0  43037  zaddcomlem  43049  zaddcom  43050  cnreeu  43076  dffltz  43180  3cubeslem2  43230  3cubeslem3l  43231  3cubeslem3r  43232  jm2.19lem3  43532  jm2.25  43540  int-addassocd  44714  binomcxplemnotnn0  44896  sub2times  45816  fperiodmullem  45846  dvnmul  46481  wallispilem4  46606  wallispi2lem2  46610  stirlinglem6  46617  dirkerper  46634  dirkertrigeqlem1  46636  dirkertrigeqlem2  46637  dirkertrigeqlem3  46638  dirkercncflem1  46641  fourierdlem26  46671  fourierdlem35  46680  fourierdlem42  46687  fourierdlem51  46695  fourierdlem64  46708  fourierdlem111  46755  hoidmv1lelem2  47130  hoidmvlelem2  47134  smflimlem4  47312  deccarry  47869  sqrtpwpw2p  48111  fmtnorec2lem  48115  fmtnorec3  48121  fmtnorec4  48122  mod42tp1mod8  48175  gpg5nbgrvtx13starlem2  48658  itcovalpclem2  49257  ackval1  49267  ackval2  49268  itscnhlc0yqe  49345  itsclquadb  49362  sinhpcosh  50325