Theorem addassd 11131

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   + caddc 11006

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

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

This theorem is referenced by:  addrid  11290  cnegex  11291  addlid  11293  addcan  11294  addcan2  11295  addcom  11296  addcomd  11312  muladd11r  11323  negeu  11347  addsubass  11367  nppcan3  11382  addsubsub23  11522  muladd  11546  add1p1  12369  div4p1lem1div2  12373  zpnn0elfzo1  13636  flhalf  13731  fldiv  13761  binom3  14128  bernneq  14133  discr1  14143  ccatass  14493  cshweqrep  14725  01sqrexlem7  15152  sqreulem  15264  isercoll2  15573  caucvgrlem  15577  iseraltlem2  15587  bcxmas  15739  bpoly4  15963  efsep  16016  efi4p  16043  efival  16058  pwp1fsum  16299  flodddiv4  16323  sadadd2lem2  16358  sadadd2lem  16367  sadasslem  16378  pcadd2  16799  prmreclem6  16830  4sqlem11  16864  vdwapun  16883  vdwlem3  16892  vdwlem6  16895  vdwlem8  16897  vdwlem9  16898  prmgaplem8  16967  psgnunilem2  19405  sylow1lem1  19508  efgredlemc  19655  psdmul  22079  opnreen  24745  ovolunlem1a  25422  nulmbl2  25462  unmbl  25463  volinun  25472  uniioombllem5  25513  itgcnlem  25716  ditgsplit  25787  dvnadd  25856  dvntaylp  26304  ulmshft  26324  ulmcn  26333  tangtx  26439  heron  26773  quad2  26774  dcubic1lem  26778  mcubic  26782  binom4  26785  dquartlem1  26786  dquartlem2  26787  dquart  26788  quart1  26791  quart  26796  lgamcvg2  26990  basellem2  27017  basellem3  27018  basellem8  27023  ppiub  27140  bcp1ctr  27215  bposlem9  27228  2lgslem3c  27334  2lgslem3d  27335  selberg3  27495  pntpbnd2  27523  pntibndlem2  27527  pntlemg  27534  pntlemk  27542  pntlemo  27543  axeuclidlem  28938  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  finsumvtxdg2ssteplem4  29525  wwlksnextwrd  29873  wwlksnextproplem3  29887  wwlksext2clwwlk  30032  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  smcnlem  30672  stadd3i  32223  golem1  32246  quad3d  32728  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  archirngz  33153  constrrtlc1  33740  constrrtcclem  33742  constrrtcc  33743  cos9thpiminplylem1  33790  cos9thpiminplylem2  33791  subfacval2  35219  subfaclim  35220  subfacval3  35221  faclimlem1  35775  faclim2  35780  fwddifnp1  36198  dnizphlfeqhlf  36509  dnibndlem10  36520  dnibndlem13  36523  poimirlem16  37675  itg2addnclem3  37712  itg2addnc  37713  areacirclem1  37747  aks4d1p1p2  42102  posbezout  42132  2np3bcnp1  42176  sticksstones12a  42189  bcle2d  42211  aks6d1c7lem1  42212  readdridaddlidd  42290  nnadd1com  42299  nnaddcom  42300  nnadddir  42302  resubeulem1  42407  resubeulem2  42408  readdsub  42416  resubsub4  42421  resubidaddlidlem  42426  sn-addlid  42436  renegneg  42444  readdcan2  42445  renegid2  42446  sn-it0e0  42448  sn-negex12  42449  sn-addcand  42452  sn-addrid  42453  sn-addcan2d  42454  sn-subeu  42459  sn-0tie0  42483  zaddcomlem  42495  zaddcom  42496  cnreeu  42522  dffltz  42666  3cubeslem2  42717  3cubeslem3l  42718  3cubeslem3r  42719  jm2.19lem3  43023  jm2.25  43031  int-addassocd  44206  binomcxplemnotnn0  44388  sub2times  45313  fperiodmullem  45343  dvnmul  45980  wallispilem4  46105  wallispi2lem2  46109  stirlinglem6  46116  dirkerper  46133  dirkertrigeqlem1  46135  dirkertrigeqlem2  46136  dirkertrigeqlem3  46137  dirkercncflem1  46140  fourierdlem26  46170  fourierdlem35  46179  fourierdlem42  46186  fourierdlem51  46194  fourierdlem64  46207  fourierdlem111  46254  hoidmv1lelem2  46629  hoidmvlelem2  46633  smflimlem4  46811  deccarry  47341  sqrtpwpw2p  47568  fmtnorec2lem  47572  fmtnorec3  47578  fmtnorec4  47579  mod42tp1mod8  47632  gpg5nbgrvtx13starlem2  48102  itcovalpclem2  48702  ackval1  48712  ackval2  48713  itscnhlc0yqe  48790  itsclquadb  48807  sinhpcosh  49771