Theorem addassd 11186

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   + caddc 11063

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089

This theorem is referenced by:  addrid  11344  cnegex  11345  addlid  11347  addcan  11348  addcan2  11349  addcom  11350  addcomd  11366  muladd11r  11377  negeu  11400  addsubass  11420  nppcan3  11434  muladd  11596  add1p1  12413  div4p1lem1div2  12417  zpnn0elfzo1  13656  flhalf  13745  fldiv  13775  binom3  14137  bernneq  14142  discr1  14152  ccatass  14488  cshweqrep  14721  01sqrexlem7  15145  sqreulem  15256  isercoll2  15565  caucvgrlem  15569  iseraltlem2  15579  bcxmas  15731  bpoly4  15953  efsep  16003  efi4p  16030  efival  16045  pwp1fsum  16284  flodddiv4  16306  sadadd2lem2  16341  sadadd2lem  16350  sadasslem  16361  pcadd2  16773  prmreclem6  16804  4sqlem11  16838  vdwapun  16857  vdwlem3  16866  vdwlem6  16869  vdwlem8  16871  vdwlem9  16872  prmgaplem8  16941  psgnunilem2  19291  sylow1lem1  19394  efgredlemc  19541  opnreen  24231  ovolunlem1a  24897  nulmbl2  24937  unmbl  24938  volinun  24947  uniioombllem5  24988  itgcnlem  25191  ditgsplit  25262  dvnadd  25330  dvntaylp  25767  ulmshft  25786  ulmcn  25795  tangtx  25899  heron  26225  quad2  26226  dcubic1lem  26230  mcubic  26234  binom4  26237  dquartlem1  26238  dquartlem2  26239  dquart  26240  quart1  26243  quart  26248  lgamcvg2  26441  basellem2  26468  basellem3  26469  basellem8  26474  ppiub  26589  bcp1ctr  26664  bposlem9  26677  2lgslem3c  26783  2lgslem3d  26784  selberg3  26944  pntpbnd2  26972  pntibndlem2  26976  pntlemg  26983  pntlemk  26991  pntlemo  26992  axeuclidlem  27974  axcontlem2  27977  axcontlem4  27979  axcontlem7  27982  finsumvtxdg2ssteplem4  28559  wwlksnextwrd  28905  wwlksnextproplem3  28919  wwlksext2clwwlk  29064  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  smcnlem  29702  stadd3i  31253  golem1  31276  cycpmco2lem3  32047  cycpmco2lem4  32048  cycpmco2lem5  32049  cycpmco2lem6  32050  cycpmco2  32052  archirngz  32095  subfacval2  33868  subfaclim  33869  subfacval3  33870  faclimlem1  34402  faclim2  34407  fwddifnp1  34826  dnizphlfeqhlf  35015  dnibndlem10  35026  dnibndlem13  35029  poimirlem16  36167  itg2addnclem3  36204  itg2addnc  36205  areacirclem1  36239  aks4d1p1p2  40600  2np3bcnp1  40625  sticksstones12a  40638  2xp3dxp2ge1d  40687  readdridaddlidd  40838  nnadd1com  40841  nnaddcom  40842  nnadddir  40844  resubeulem1  40902  resubeulem2  40903  readdsub  40911  resubsub4  40916  resubidaddlidlem  40921  sn-addlid  40931  renegneg  40938  readdcan2  40939  renegid2  40940  sn-it0e0  40942  sn-negex12  40943  sn-addcand  40946  sn-addrid  40947  sn-addcan2d  40948  sn-subeu  40953  sn-0tie0  40966  zaddcomlem  40978  zaddcom  40979  cnreeu  40995  dffltz  41030  3cubeslem2  41066  3cubeslem3l  41067  3cubeslem3r  41068  jm2.19lem3  41373  jm2.25  41381  int-addassocd  42569  binomcxplemnotnn0  42758  sub2times  43627  fperiodmullem  43658  dvnmul  44304  wallispilem4  44429  wallispi2lem2  44433  stirlinglem6  44440  dirkerper  44457  dirkertrigeqlem1  44459  dirkertrigeqlem2  44460  dirkertrigeqlem3  44461  dirkercncflem1  44464  fourierdlem26  44494  fourierdlem35  44503  fourierdlem42  44510  fourierdlem51  44518  fourierdlem64  44531  fourierdlem111  44578  hoidmv1lelem2  44953  hoidmvlelem2  44957  smflimlem4  45135  deccarry  45663  sqrtpwpw2p  45850  fmtnorec2lem  45854  fmtnorec3  45860  fmtnorec4  45861  mod42tp1mod8  45914  itcovalpclem2  46877  ackval1  46887  ackval2  46888  itscnhlc0yqe  46965  itsclquadb  46982  sinhpcosh  47305