Theorem addassd 9941

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  addid1  10095  cnegex  10096  addid2  10098  addcan  10099  addcan2  10100  addcom  10101  addcomd  10117  muladd11r  10128  negeu  10150  addsubass  10170  nppcan3  10184  muladd  10341  add1p1  11160  div4p1lem1div2  11164  zpnn0elfzo1  12408  flhalf  12493  fldiv  12521  binom3  12847  bernneq  12852  discr1  12862  ccatass  13224  cshweqrep  13418  sqrlem7  13837  sqreulem  13947  isercoll2  14247  caucvgrlem  14251  iseraltlem2  14261  bcxmas  14406  bpoly4  14629  efsep  14679  efi4p  14706  efival  14721  pwp1fsum  14952  flodddiv4  14975  sadadd2lem2  15010  sadadd2lem  15019  sadasslem  15030  pcadd2  15432  prmreclem6  15463  4sqlem11  15497  vdwapun  15516  vdwlem3  15525  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  prmgaplem8  15600  psgnunilem2  17738  sylow1lem1  17836  efgredlemc  17981  opnreen  22442  ovolunlem1a  23071  nulmbl2  23111  unmbl  23112  volinun  23121  uniioombllem5  23161  itgcnlem  23362  ditgsplit  23431  dvnadd  23498  dvntaylp  23929  ulmshft  23948  ulmcn  23957  tangtx  24061  heron  24365  quad2  24366  dcubic1lem  24370  mcubic  24374  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1  24383  quart  24388  lgamcvg2  24581  basellem2  24608  basellem3  24609  basellem8  24614  ppiub  24729  bcp1ctr  24804  bposlem9  24817  2lgslem3c  24923  2lgslem3d  24924  selberg3  25048  pntpbnd2  25076  pntibndlem2  25080  pntlemg  25087  pntlemk  25095  pntlemo  25096  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  wwlkextwrd  26256  wwlkextproplem3  26271  wwlkext2clwwlk  26331  numclwlk1lem2fo  26622  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  smcnlem  26936  stadd3i  28491  golem1  28514  archirngz  29074  subfacval2  30423  subfaclim  30424  subfacval3  30425  faclimlem1  30882  faclim2  30887  fwddifnp1  31442  dnizphlfeqhlf  31636  dnibndlem10  31647  dnibndlem13  31650  poimirlem16  32595  itg2addnclem3  32633  itg2addnc  32634  areacirclem1  32670  jm2.19lem3  36576  jm2.25  36584  int-addassocd  37499  binomcxplemnotnn0  37577  sub2times  38426  fperiodmullem  38458  dvnmul  38833  wallispilem4  38961  wallispi2lem2  38965  stirlinglem6  38972  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkercncflem1  38996  fourierdlem26  39026  fourierdlem35  39035  fourierdlem42  39042  fourierdlem51  39050  fourierdlem64  39063  fourierdlem111  39110  hoidmv1lelem2  39482  hoidmvlelem2  39486  smflimlem4  39660  deccarry  39941  sqrtpwpw2p  39988  fmtnorec2lem  39992  fmtnorec3  39998  fmtnorec4  39999  mod42tp1mod8  40057  wwlksnextwrd  41103  wwlksnextproplem3  41117  wwlksext2clwwlk  41231  av-numclwlk1lem2fo  41525  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  sinhpcosh  42280