Theorem addassd 11156

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11314  cnegex  11315  addlid  11317  addcan  11318  addcan2  11319  addcom  11320  addcomd  11336  muladd11r  11347  negeu  11371  addsubass  11391  nppcan3  11406  addsubsub23  11546  muladd  11570  add1p1  12393  div4p1lem1div2  12397  zpnn0elfzo1  13660  flhalf  13752  fldiv  13782  binom3  14149  bernneq  14154  discr1  14164  ccatass  14513  cshweqrep  14745  01sqrexlem7  15173  sqreulem  15285  isercoll2  15594  caucvgrlem  15598  iseraltlem2  15608  bcxmas  15760  bpoly4  15984  efsep  16037  efi4p  16064  efival  16079  pwp1fsum  16320  flodddiv4  16344  sadadd2lem2  16379  sadadd2lem  16388  sadasslem  16399  pcadd2  16820  prmreclem6  16851  4sqlem11  16885  vdwapun  16904  vdwlem3  16913  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  prmgaplem8  16988  psgnunilem2  19392  sylow1lem1  19495  efgredlemc  19642  psdmul  22069  opnreen  24736  ovolunlem1a  25413  nulmbl2  25453  unmbl  25454  volinun  25463  uniioombllem5  25504  itgcnlem  25707  ditgsplit  25778  dvnadd  25847  dvntaylp  26295  ulmshft  26315  ulmcn  26324  tangtx  26430  heron  26764  quad2  26765  dcubic1lem  26769  mcubic  26773  binom4  26776  dquartlem1  26777  dquartlem2  26778  dquart  26779  quart1  26782  quart  26787  lgamcvg2  26981  basellem2  27008  basellem3  27009  basellem8  27014  ppiub  27131  bcp1ctr  27206  bposlem9  27219  2lgslem3c  27325  2lgslem3d  27326  selberg3  27486  pntpbnd2  27514  pntibndlem2  27518  pntlemg  27525  pntlemk  27533  pntlemo  27534  axeuclidlem  28925  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  finsumvtxdg2ssteplem4  29512  wwlksnextwrd  29860  wwlksnextproplem3  29874  wwlksext2clwwlk  30019  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  smcnlem  30659  stadd3i  32210  golem1  32233  quad3d  32706  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2  33088  archirngz  33141  constrrtlc1  33698  constrrtcclem  33700  constrrtcc  33701  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  subfacval2  35159  subfaclim  35160  subfacval3  35161  faclimlem1  35715  faclim2  35720  fwddifnp1  36138  dnizphlfeqhlf  36449  dnibndlem10  36460  dnibndlem13  36463  poimirlem16  37615  itg2addnclem3  37652  itg2addnc  37653  areacirclem1  37687  aks4d1p1p2  42043  posbezout  42073  2np3bcnp1  42117  sticksstones12a  42130  bcle2d  42152  aks6d1c7lem1  42153  readdridaddlidd  42231  nnadd1com  42240  nnaddcom  42241  nnadddir  42243  resubeulem1  42348  resubeulem2  42349  readdsub  42357  resubsub4  42362  resubidaddlidlem  42367  sn-addlid  42377  renegneg  42385  readdcan2  42386  renegid2  42387  sn-it0e0  42389  sn-negex12  42390  sn-addcand  42393  sn-addrid  42394  sn-addcan2d  42395  sn-subeu  42400  sn-0tie0  42424  zaddcomlem  42436  zaddcom  42437  cnreeu  42463  dffltz  42607  3cubeslem2  42658  3cubeslem3l  42659  3cubeslem3r  42660  jm2.19lem3  42964  jm2.25  42972  int-addassocd  44147  binomcxplemnotnn0  44329  sub2times  45255  fperiodmullem  45285  dvnmul  45925  wallispilem4  46050  wallispi2lem2  46054  stirlinglem6  46061  dirkerper  46078  dirkertrigeqlem1  46080  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkercncflem1  46085  fourierdlem26  46115  fourierdlem35  46124  fourierdlem42  46131  fourierdlem51  46139  fourierdlem64  46152  fourierdlem111  46199  hoidmv1lelem2  46574  hoidmvlelem2  46578  smflimlem4  46756  deccarry  47296  sqrtpwpw2p  47523  fmtnorec2lem  47527  fmtnorec3  47533  fmtnorec4  47534  mod42tp1mod8  47587  gpg5nbgrvtx13starlem2  48057  itcovalpclem2  48657  ackval1  48667  ackval2  48668  itscnhlc0yqe  48745  itsclquadb  48762  sinhpcosh  49726