Theorem addassd 11158

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032

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

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

This theorem is referenced by:  addrid  11317  cnegex  11318  addlid  11320  addcan  11321  addcan2  11322  addcom  11323  addcomd  11339  muladd11r  11350  negeu  11374  addsubass  11394  nppcan3  11409  addsubsub23  11549  muladd  11573  nnadd1com  12191  nnaddcom  12192  nnadddir  12224  add1p1  12419  div4p1lem1div2  12423  zpnn0elfzo1  13685  flhalf  13780  fldiv  13810  binom3  14177  bernneq  14182  discr1  14192  ccatass  14542  cshweqrep  14774  01sqrexlem7  15201  sqreulem  15313  isercoll2  15622  caucvgrlem  15626  iseraltlem2  15636  bcxmas  15791  bpoly4  16015  efsep  16068  efi4p  16095  efival  16110  pwp1fsum  16351  flodddiv4  16375  sadadd2lem2  16410  sadadd2lem  16419  sadasslem  16430  pcadd2  16852  prmreclem6  16883  4sqlem11  16917  vdwapun  16936  vdwlem3  16945  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  prmgaplem8  17020  psgnunilem2  19461  sylow1lem1  19564  efgredlemc  19711  psdmul  22142  opnreen  24807  ovolunlem1a  25473  nulmbl2  25513  unmbl  25514  volinun  25523  uniioombllem5  25564  itgcnlem  25767  ditgsplit  25838  dvnadd  25906  dvntaylp  26348  ulmshft  26368  ulmcn  26377  tangtx  26482  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  27181  bcp1ctr  27256  bposlem9  27269  2lgslem3c  27375  2lgslem3d  27376  selberg3  27536  pntpbnd2  27564  pntibndlem2  27568  pntlemg  27575  pntlemk  27583  pntlemo  27584  axeuclidlem  29045  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  finsumvtxdg2ssteplem4  29632  wwlksnextwrd  29980  wwlksnextproplem3  29994  wwlksext2clwwlk  30142  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  smcnlem  30783  stadd3i  32334  golem1  32357  quad3d  32837  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2  33209  archirngz  33265  constrrtlc1  33892  constrrtcclem  33894  constrrtcc  33895  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  subfacval2  35385  subfaclim  35386  subfacval3  35387  faclimlem1  35941  faclim2  35946  fwddifnp1  36363  dnizphlfeqhlf  36752  dnibndlem10  36763  dnibndlem13  36766  poimirlem16  37971  itg2addnclem3  38008  itg2addnc  38009  areacirclem1  38043  aks4d1p1p2  42523  posbezout  42553  2np3bcnp1  42597  sticksstones12a  42610  bcle2d  42632  aks6d1c7lem1  42633  readdridaddlidd  42710  resubeulem1  42821  resubeulem2  42822  readdsub  42830  resubsub4  42835  resubidaddlidlem  42840  sn-addlid  42850  renegneg  42858  readdcan2  42859  renegid2  42860  sn-it0e0  42862  sn-negex12  42863  sn-addcand  42866  sn-addrid  42867  sn-addcan2d  42868  sn-subeu  42873  sn-0tie0  42910  zaddcomlem  42922  zaddcom  42923  cnreeu  42949  dffltz  43081  3cubeslem2  43131  3cubeslem3l  43132  3cubeslem3r  43133  jm2.19lem3  43437  jm2.25  43445  int-addassocd  44619  binomcxplemnotnn0  44801  sub2times  45724  fperiodmullem  45754  dvnmul  46389  wallispilem4  46514  wallispi2lem2  46518  stirlinglem6  46525  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkercncflem1  46549  fourierdlem26  46579  fourierdlem35  46588  fourierdlem42  46595  fourierdlem51  46603  fourierdlem64  46616  fourierdlem111  46663  hoidmv1lelem2  47038  hoidmvlelem2  47042  smflimlem4  47220  deccarry  47771  sqrtpwpw2p  48013  fmtnorec2lem  48017  fmtnorec3  48023  fmtnorec4  48024  mod42tp1mod8  48077  gpg5nbgrvtx13starlem2  48560  itcovalpclem2  49159  ackval1  49169  ackval2  49170  itscnhlc0yqe  49247  itsclquadb  49264  sinhpcosh  50227