Theorem addassd 11268

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138   + caddc 11143

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086

This theorem is referenced by:  addrid  11426  cnegex  11427  addlid  11429  addcan  11430  addcan2  11431  addcom  11432  addcomd  11448  muladd11r  11459  negeu  11482  addsubass  11502  nppcan3  11516  muladd  11678  add1p1  12496  div4p1lem1div2  12500  zpnn0elfzo1  13741  flhalf  13831  fldiv  13861  binom3  14222  bernneq  14227  discr1  14237  ccatass  14574  cshweqrep  14807  01sqrexlem7  15231  sqreulem  15342  isercoll2  15651  caucvgrlem  15655  iseraltlem2  15665  bcxmas  15817  bpoly4  16039  efsep  16090  efi4p  16117  efival  16132  pwp1fsum  16371  flodddiv4  16393  sadadd2lem2  16428  sadadd2lem  16437  sadasslem  16448  pcadd2  16862  prmreclem6  16893  4sqlem11  16927  vdwapun  16946  vdwlem3  16955  vdwlem6  16958  vdwlem8  16960  vdwlem9  16961  prmgaplem8  17030  psgnunilem2  19462  sylow1lem1  19565  efgredlemc  19712  psdmul  22113  opnreen  24791  ovolunlem1a  25469  nulmbl2  25509  unmbl  25510  volinun  25519  uniioombllem5  25560  itgcnlem  25763  ditgsplit  25834  dvnadd  25903  dvntaylp  26351  ulmshft  26371  ulmcn  26380  tangtx  26485  heron  26815  quad2  26816  dcubic1lem  26820  mcubic  26824  binom4  26827  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1  26833  quart  26838  lgamcvg2  27032  basellem2  27059  basellem3  27060  basellem8  27065  ppiub  27182  bcp1ctr  27257  bposlem9  27270  2lgslem3c  27376  2lgslem3d  27377  selberg3  27537  pntpbnd2  27565  pntibndlem2  27569  pntlemg  27576  pntlemk  27584  pntlemo  27585  axeuclidlem  28845  axcontlem2  28848  axcontlem4  28850  axcontlem7  28853  finsumvtxdg2ssteplem4  29434  wwlksnextwrd  29780  wwlksnextproplem3  29794  wwlksext2clwwlk  29939  numclwlk2lem2f  30259  numclwlk2lem2f1o  30261  smcnlem  30579  stadd3i  32130  golem1  32153  cycpmco2lem3  32941  cycpmco2lem4  32942  cycpmco2lem5  32943  cycpmco2lem6  32944  cycpmco2  32946  archirngz  32989  subfacval2  34925  subfaclim  34926  subfacval3  34927  faclimlem1  35465  faclim2  35470  fwddifnp1  35889  dnizphlfeqhlf  36079  dnibndlem10  36090  dnibndlem13  36093  poimirlem16  37237  itg2addnclem3  37274  itg2addnc  37275  areacirclem1  37309  aks4d1p1p2  41670  posbezout  41700  2np3bcnp1  41744  sticksstones12a  41757  bcle2d  41779  aks6d1c7lem1  41780  2xp3dxp2ge1d  41824  readdridaddlidd  41971  nnadd1com  41974  nnaddcom  41975  nnadddir  41977  resubeulem1  42062  resubeulem2  42063  readdsub  42071  resubsub4  42076  resubidaddlidlem  42081  sn-addlid  42091  renegneg  42098  readdcan2  42099  renegid2  42100  sn-it0e0  42102  sn-negex12  42103  sn-addcand  42106  sn-addrid  42107  sn-addcan2d  42108  sn-subeu  42113  sn-0tie0  42126  zaddcomlem  42138  zaddcom  42139  cnreeu  42155  dffltz  42190  3cubeslem2  42244  3cubeslem3l  42245  3cubeslem3r  42246  jm2.19lem3  42551  jm2.25  42559  int-addassocd  43743  binomcxplemnotnn0  43932  sub2times  44789  fperiodmullem  44820  dvnmul  45466  wallispilem4  45591  wallispi2lem2  45595  stirlinglem6  45602  dirkerper  45619  dirkertrigeqlem1  45621  dirkertrigeqlem2  45622  dirkertrigeqlem3  45623  dirkercncflem1  45626  fourierdlem26  45656  fourierdlem35  45665  fourierdlem42  45672  fourierdlem51  45680  fourierdlem64  45693  fourierdlem111  45740  hoidmv1lelem2  46115  hoidmvlelem2  46119  smflimlem4  46297  deccarry  46826  sqrtpwpw2p  47012  fmtnorec2lem  47016  fmtnorec3  47022  fmtnorec4  47023  mod42tp1mod8  47076  itcovalpclem2  47927  ackval1  47937  ackval2  47938  itscnhlc0yqe  48015  itsclquadb  48032  sinhpcosh  48354