Theorem addassd 11334

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   + caddc 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11493  cnegex  11494  addlid  11496  addcan  11497  addcan2  11498  addcom  11499  addcomd  11515  muladd11r  11526  negeu  11550  addsubass  11570  nppcan3  11585  addsubsub23  11725  muladd  11751  nnadd1com  12364  nnaddcom  12365  nnadddir  12397  add1p1  12600  div4p1lem1div2  12604  zpnn0elfzo1  13877  flhalf  13973  fldiv  14003  binom3  14371  bernneq  14376  discr1  14386  ccatass  14737  cshweqrep  14976  01sqrexlem7  15420  sqreulem  15532  isercoll2  15841  caucvgrlem  15845  iseraltlem2  15855  bcxmas  16009  bpoly4  16230  efsep  16283  efi4p  16310  efival  16325  pwp1fsum  16566  flodddiv4  16590  sadadd2lem2  16625  sadadd2lem  16634  sadasslem  16645  pcadd2  17073  prmreclem6  17104  4sqlem11  17138  vdwapun  17157  vdwlem3  17166  vdwlem6  17169  vdwlem8  17171  vdwlem9  17172  prmgaplem8  17241  psgnunilem2  19714  sylow1lem1  19817  efgredlemc  19964  psdmul  22492  opnreen  25156  ovolunlem1a  25822  nulmbl2  25862  unmbl  25863  volinun  25872  uniioombllem5  25913  itgcnlem  26115  ditgsplit  26186  dvnadd  26254  dvntaylp  26703  ulmshft  26722  ulmcn  26731  tangtx  26839  heron  27171  quad2  27172  dcubic1lem  27176  mcubic  27180  binom4  27183  dquartlem1  27184  dquartlem2  27185  dquart  27186  quart1  27189  quart  27194  lgamcvg2  27387  basellem2  27414  basellem3  27415  basellem8  27420  ppiub  27536  bcp1ctr  27611  bposlem9  27624  2lgslem3c  27730  2lgslem3d  27731  selberg3  27891  pntpbnd2  27919  pntibndlem2  27923  pntlemg  27930  pntlemk  27938  pntlemo  27939  axeuclidlem  29545  axcontlem2  29548  axcontlem4  29550  axcontlem7  29553  finsumvtxdg2ssteplem4  30134  wwlksnextwrd  30491  wwlksnextproplem3  30505  wwlksext2clwwlk  30653  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  smcnlem  31304  stadd3i  32855  golem1  32878  quad3d  33387  cycpmco2lem3  33735  cycpmco2lem4  33736  cycpmco2lem5  33737  cycpmco2lem6  33738  cycpmco2  33740  archirngz  33796  constrrtlc1  34410  constrrtcclem  34412  constrrtcc  34413  cos9thpiminplylem1  34460  cos9thpiminplylem2  34461  subfacval2  36038  subfaclim  36039  subfacval3  36040  faclimlem1  36600  faclim2  36605  fwddifnp1  37022  dnizphlfeqhlf  37434  dnibndlem10  37445  dnibndlem13  37448  qdiff  38341  poimirlem16  38647  itg2addnclem3  38684  itg2addnc  38685  areacirclem1  38719  aks4d1p1p2  43213  posbezout  43243  2np3bcnp1  43287  sticksstones12a  43300  bcle2d  43322  aks6d1c7lem1  43323  quadfac  43348  readdridaddlidd  43401  resubeulem1  43519  resubeulem2  43520  readdsub  43528  resubsub4  43533  resubidaddlidlem  43538  sn-addlid  43548  renegneg  43556  readdcan2  43557  renegid2  43558  sn-it0e0  43560  sn-negex12  43561  sn-addcand  43564  sn-addrid  43565  sn-addcan2d  43566  sn-subeu  43571  sn-0tie0  43608  zaddcomlem  43620  zaddcom  43621  cnreeu  43647  dffltz  43763  3cubeslem2  43788  3cubeslem3l  43789  3cubeslem3r  43790  jm2.19lem3  44091  jm2.25  44099  int-addassocd  45267  binomcxplemnotnn0  45433  sub2times  46382  fperiodmullem  46412  dvnmul  47046  wallispilem4  47171  wallispi2lem2  47175  stirlinglem6  47182  dirkerper  47199  dirkertrigeqlem1  47201  dirkertrigeqlem2  47202  dirkertrigeqlem3  47203  dirkercncflem1  47206  fourierdlem26  47236  fourierdlem35  47245  fourierdlem42  47252  fourierdlem51  47260  fourierdlem64  47273  fourierdlem111  47320  hoidmv1lelem2  47695  hoidmvlelem2  47699  smflimlem4  47877  deccarry  48474  sqrtpwpw2p  48716  fmtnorec2lem  48720  fmtnorec3  48726  fmtnorec4  48727  mod42tp1mod8  48780  gpg5nbgrvtx13starlem2  49263  itcovalpclem2  49876  ackval1  49886  ackval2  49887  itscnhlc0yqe  49964  itsclquadb  49981  sinhpcosh  51001  crosspdotsumlem  51132  crossp3d  51135  veroquadgsumlem  51151