Theorem addassd 10663

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  addid1  10820  cnegex  10821  addid2  10823  addcan  10824  addcan2  10825  addcom  10826  addcomd  10842  muladd11r  10853  negeu  10876  addsubass  10896  nppcan3  10910  muladd  11072  add1p1  11889  div4p1lem1div2  11893  zpnn0elfzo1  13112  flhalf  13201  fldiv  13229  binom3  13586  bernneq  13591  discr1  13601  ccatass  13942  cshweqrep  14183  sqrlem7  14608  sqreulem  14719  isercoll2  15025  caucvgrlem  15029  iseraltlem2  15039  bcxmas  15190  bpoly4  15413  efsep  15463  efi4p  15490  efival  15505  pwp1fsum  15742  flodddiv4  15764  sadadd2lem2  15799  sadadd2lem  15808  sadasslem  15819  pcadd2  16226  prmreclem6  16257  4sqlem11  16291  vdwapun  16310  vdwlem3  16319  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  prmgaplem8  16394  psgnunilem2  18623  sylow1lem1  18723  efgredlemc  18871  opnreen  23439  ovolunlem1a  24097  nulmbl2  24137  unmbl  24138  volinun  24147  uniioombllem5  24188  itgcnlem  24390  ditgsplit  24459  dvnadd  24526  dvntaylp  24959  ulmshft  24978  ulmcn  24987  tangtx  25091  heron  25416  quad2  25417  dcubic1lem  25421  mcubic  25425  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1  25434  quart  25439  lgamcvg2  25632  basellem2  25659  basellem3  25660  basellem8  25665  ppiub  25780  bcp1ctr  25855  bposlem9  25868  2lgslem3c  25974  2lgslem3d  25975  selberg3  26135  pntpbnd2  26163  pntibndlem2  26167  pntlemg  26174  pntlemk  26182  pntlemo  26183  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  finsumvtxdg2ssteplem4  27330  wwlksnextwrd  27675  wwlksnextproplem3  27690  wwlksext2clwwlk  27836  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  smcnlem  28474  stadd3i  30025  golem1  30048  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2  30775  archirngz  30818  subfacval2  32434  subfaclim  32435  subfacval3  32436  faclimlem1  32975  faclim2  32980  fwddifnp1  33626  dnizphlfeqhlf  33815  dnibndlem10  33826  dnibndlem13  33829  poimirlem16  34923  itg2addnclem3  34960  itg2addnc  34961  areacirclem1  34997  2xp3dxp2ge1d  39146  readdid1addid2d  39206  nnadd1com  39209  nnaddcom  39210  nnadddir  39212  resubeulem1  39254  resubeulem2  39255  readdsub  39263  resubsub4  39268  resubidaddid1lem  39273  sn-addid2  39283  renegneg  39290  readdcan2  39291  dffltz  39320  3cubeslem2  39331  3cubeslem3l  39332  3cubeslem3r  39333  jm2.19lem3  39637  jm2.25  39645  int-addassocd  40576  binomcxplemnotnn0  40737  sub2times  41589  fperiodmullem  41619  dvnmul  42277  wallispilem4  42402  wallispi2lem2  42406  stirlinglem6  42413  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  dirkercncflem1  42437  fourierdlem26  42467  fourierdlem35  42476  fourierdlem42  42483  fourierdlem51  42491  fourierdlem64  42504  fourierdlem111  42551  hoidmv1lelem2  42923  hoidmvlelem2  42927  smflimlem4  43099  deccarry  43560  sqrtpwpw2p  43749  fmtnorec2lem  43753  fmtnorec3  43759  fmtnorec4  43760  mod42tp1mod8  43816  itscnhlc0yqe  44795  itsclquadb  44812  sinhpcosh  44888