Theorem addassd 11283

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158

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

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

This theorem is referenced by:  addrid  11441  cnegex  11442  addlid  11444  addcan  11445  addcan2  11446  addcom  11447  addcomd  11463  muladd11r  11474  negeu  11498  addsubass  11518  nppcan3  11533  muladd  11695  add1p1  12517  div4p1lem1div2  12521  zpnn0elfzo1  13778  flhalf  13870  fldiv  13900  binom3  14263  bernneq  14268  discr1  14278  ccatass  14626  cshweqrep  14859  01sqrexlem7  15287  sqreulem  15398  isercoll2  15705  caucvgrlem  15709  iseraltlem2  15719  bcxmas  15871  bpoly4  16095  efsep  16146  efi4p  16173  efival  16188  pwp1fsum  16428  flodddiv4  16452  sadadd2lem2  16487  sadadd2lem  16496  sadasslem  16507  pcadd2  16928  prmreclem6  16959  4sqlem11  16993  vdwapun  17012  vdwlem3  17021  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  prmgaplem8  17096  psgnunilem2  19513  sylow1lem1  19616  efgredlemc  19763  psdmul  22170  opnreen  24853  ovolunlem1a  25531  nulmbl2  25571  unmbl  25572  volinun  25581  uniioombllem5  25622  itgcnlem  25825  ditgsplit  25896  dvnadd  25965  dvntaylp  26413  ulmshft  26433  ulmcn  26442  tangtx  26547  heron  26881  quad2  26882  dcubic1lem  26886  mcubic  26890  binom4  26893  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1  26899  quart  26904  lgamcvg2  27098  basellem2  27125  basellem3  27126  basellem8  27131  ppiub  27248  bcp1ctr  27323  bposlem9  27336  2lgslem3c  27442  2lgslem3d  27443  selberg3  27603  pntpbnd2  27631  pntibndlem2  27635  pntlemg  27642  pntlemk  27650  pntlemo  27651  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  finsumvtxdg2ssteplem4  29566  wwlksnextwrd  29917  wwlksnextproplem3  29931  wwlksext2clwwlk  30076  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  smcnlem  30716  stadd3i  32267  golem1  32290  quad3d  32754  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  archirngz  33196  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  subfacval2  35192  subfaclim  35193  subfacval3  35194  faclimlem1  35743  faclim2  35748  fwddifnp1  36166  dnizphlfeqhlf  36477  dnibndlem10  36488  dnibndlem13  36491  poimirlem16  37643  itg2addnclem3  37680  itg2addnc  37681  areacirclem1  37715  aks4d1p1p2  42071  posbezout  42101  2np3bcnp1  42145  sticksstones12a  42158  bcle2d  42180  aks6d1c7lem1  42181  2xp3dxp2ge1d  42242  readdridaddlidd  42299  nnadd1com  42302  nnaddcom  42303  nnadddir  42305  resubeulem1  42405  resubeulem2  42406  readdsub  42414  resubsub4  42419  resubidaddlidlem  42424  sn-addlid  42434  renegneg  42441  readdcan2  42442  renegid2  42443  sn-it0e0  42445  sn-negex12  42446  sn-addcand  42449  sn-addrid  42450  sn-addcan2d  42451  sn-subeu  42456  sn-0tie0  42469  zaddcomlem  42481  zaddcom  42482  cnreeu  42500  dffltz  42644  3cubeslem2  42696  3cubeslem3l  42697  3cubeslem3r  42698  jm2.19lem3  43003  jm2.25  43011  int-addassocd  44187  binomcxplemnotnn0  44375  sub2times  45284  fperiodmullem  45315  dvnmul  45958  wallispilem4  46083  wallispi2lem2  46087  stirlinglem6  46094  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem1  46118  fourierdlem26  46148  fourierdlem35  46157  fourierdlem42  46164  fourierdlem51  46172  fourierdlem64  46185  fourierdlem111  46232  hoidmv1lelem2  46607  hoidmvlelem2  46611  smflimlem4  46789  deccarry  47323  sqrtpwpw2p  47525  fmtnorec2lem  47529  fmtnorec3  47535  fmtnorec4  47536  mod42tp1mod8  47589  gpg5nbgrvtx13starlem2  48028  itcovalpclem2  48592  ackval1  48602  ackval2  48603  itscnhlc0yqe  48680  itsclquadb  48697  sinhpcosh  49259