Theorem addassd 11280

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   + caddc 11155

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

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

This theorem is referenced by:  addrid  11438  cnegex  11439  addlid  11441  addcan  11442  addcan2  11443  addcom  11444  addcomd  11460  muladd11r  11471  negeu  11495  addsubass  11515  nppcan3  11530  muladd  11692  add1p1  12514  div4p1lem1div2  12518  zpnn0elfzo1  13774  flhalf  13866  fldiv  13896  binom3  14259  bernneq  14264  discr1  14274  ccatass  14622  cshweqrep  14855  01sqrexlem7  15283  sqreulem  15394  isercoll2  15701  caucvgrlem  15705  iseraltlem2  15715  bcxmas  15867  bpoly4  16091  efsep  16142  efi4p  16169  efival  16184  pwp1fsum  16424  flodddiv4  16448  sadadd2lem2  16483  sadadd2lem  16492  sadasslem  16503  pcadd2  16923  prmreclem6  16954  4sqlem11  16988  vdwapun  17007  vdwlem3  17016  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  prmgaplem8  17091  psgnunilem2  19527  sylow1lem1  19630  efgredlemc  19777  psdmul  22187  opnreen  24866  ovolunlem1a  25544  nulmbl2  25584  unmbl  25585  volinun  25594  uniioombllem5  25635  itgcnlem  25839  ditgsplit  25910  dvnadd  25979  dvntaylp  26427  ulmshft  26447  ulmcn  26456  tangtx  26561  heron  26895  quad2  26896  dcubic1lem  26900  mcubic  26904  binom4  26907  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1  26913  quart  26918  lgamcvg2  27112  basellem2  27139  basellem3  27140  basellem8  27145  ppiub  27262  bcp1ctr  27337  bposlem9  27350  2lgslem3c  27456  2lgslem3d  27457  selberg3  27617  pntpbnd2  27645  pntibndlem2  27649  pntlemg  27656  pntlemk  27664  pntlemo  27665  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  finsumvtxdg2ssteplem4  29580  wwlksnextwrd  29926  wwlksnextproplem3  29940  wwlksext2clwwlk  30085  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  smcnlem  30725  stadd3i  32276  golem1  32299  quad3d  32760  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  archirngz  33178  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  subfacval2  35171  subfaclim  35172  subfacval3  35173  faclimlem1  35722  faclim2  35727  fwddifnp1  36146  dnizphlfeqhlf  36458  dnibndlem10  36469  dnibndlem13  36472  poimirlem16  37622  itg2addnclem3  37659  itg2addnc  37660  areacirclem1  37694  aks4d1p1p2  42051  posbezout  42081  2np3bcnp1  42125  sticksstones12a  42138  bcle2d  42160  aks6d1c7lem1  42161  2xp3dxp2ge1d  42222  readdridaddlidd  42277  nnadd1com  42280  nnaddcom  42281  nnadddir  42283  resubeulem1  42381  resubeulem2  42382  readdsub  42390  resubsub4  42395  resubidaddlidlem  42400  sn-addlid  42410  renegneg  42417  readdcan2  42418  renegid2  42419  sn-it0e0  42421  sn-negex12  42422  sn-addcand  42425  sn-addrid  42426  sn-addcan2d  42427  sn-subeu  42432  sn-0tie0  42445  zaddcomlem  42457  zaddcom  42458  cnreeu  42476  dffltz  42620  3cubeslem2  42672  3cubeslem3l  42673  3cubeslem3r  42674  jm2.19lem3  42979  jm2.25  42987  int-addassocd  44163  binomcxplemnotnn0  44351  sub2times  45222  fperiodmullem  45253  dvnmul  45898  wallispilem4  46023  wallispi2lem2  46027  stirlinglem6  46034  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem1  46058  fourierdlem26  46088  fourierdlem35  46097  fourierdlem42  46104  fourierdlem51  46112  fourierdlem64  46125  fourierdlem111  46172  hoidmv1lelem2  46547  hoidmvlelem2  46551  smflimlem4  46729  deccarry  47260  sqrtpwpw2p  47462  fmtnorec2lem  47466  fmtnorec3  47472  fmtnorec4  47473  mod42tp1mod8  47526  gpg5nbgrvtx13starlem2  47962  itcovalpclem2  48520  ackval1  48530  ackval2  48531  itscnhlc0yqe  48608  itsclquadb  48625  sinhpcosh  48970