Theorem addassd 11249

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121

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

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

This theorem is used by:  addrid  11408  cnegex  11409  addlid  11411  addcan  11412  addcan2  11413  addcom  11414  addcomd  11430  muladd11r  11441  negeu  11465  addsubass  11485  nppcan3  11500  addsubsub23  11640  muladd  11664  nnadd1com  12277  nnaddcom  12278  nnadddir  12310  add1p1  12513  div4p1lem1div2  12517  zpnn0elfzo1  13787  flhalf  13883  fldiv  13913  binom3  14280  bernneq  14285  discr1  14295  ccatass  14646  cshweqrep  14884  01sqrexlem7  15325  sqreulem  15437  isercoll2  15746  caucvgrlem  15750  iseraltlem2  15760  bcxmas  15915  bpoly4  16138  efsep  16191  efi4p  16218  efival  16233  pwp1fsum  16474  flodddiv4  16498  sadadd2lem2  16533  sadadd2lem  16542  sadasslem  16553  pcadd2  16975  prmreclem6  17006  4sqlem11  17040  vdwapun  17059  vdwlem3  17068  vdwlem6  17071  vdwlem8  17073  vdwlem9  17074  prmgaplem8  17143  psgnunilem2  19596  sylow1lem1  19699  efgredlemc  19846  psdmul  22366  opnreen  25026  ovolunlem1a  25692  nulmbl2  25732  unmbl  25733  volinun  25742  uniioombllem5  25783  itgcnlem  25986  ditgsplit  26057  dvnadd  26125  dvntaylp  26571  ulmshft  26590  ulmcn  26599  tangtx  26707  heron  27040  quad2  27041  dcubic1lem  27045  mcubic  27049  binom4  27052  dquartlem1  27053  dquartlem2  27054  dquart  27055  quart1  27058  quart  27063  lgamcvg2  27256  basellem2  27283  basellem3  27284  basellem8  27289  ppiub  27405  bcp1ctr  27480  bposlem9  27493  2lgslem3c  27599  2lgslem3d  27600  selberg3  27760  pntpbnd2  27788  pntibndlem2  27792  pntlemg  27799  pntlemk  27807  pntlemo  27808  axeuclidlem  29349  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  finsumvtxdg2ssteplem4  29935  wwlksnextwrd  30283  wwlksnextproplem3  30297  wwlksext2clwwlk  30445  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  smcnlem  31086  stadd3i  32637  golem1  32660  quad3d  33131  cycpmco2lem3  33479  cycpmco2lem4  33480  cycpmco2lem5  33481  cycpmco2lem6  33482  cycpmco2  33484  archirngz  33540  constrrtlc1  34153  constrrtcclem  34155  constrrtcc  34156  cos9thpiminplylem1  34203  cos9thpiminplylem2  34204  subfacval2  35699  subfaclim  35700  subfacval3  35701  faclimlem1  36255  faclim2  36260  fwddifnp1  36677  dnizphlfeqhlf  37105  dnibndlem10  37116  dnibndlem13  37119  qdiff  38011  poimirlem16  38327  itg2addnclem3  38364  itg2addnc  38365  areacirclem1  38399  aks4d1p1p2  42877  posbezout  42907  2np3bcnp1  42951  sticksstones12a  42964  bcle2d  42986  aks6d1c7lem1  42987  quadfac  43012  readdridaddlidd  43065  resubeulem1  43176  resubeulem2  43177  readdsub  43185  resubsub4  43190  resubidaddlidlem  43195  sn-addlid  43205  renegneg  43213  readdcan2  43214  renegid2  43215  sn-it0e0  43217  sn-negex12  43218  sn-addcand  43221  sn-addrid  43222  sn-addcan2d  43223  sn-subeu  43228  sn-0tie0  43265  zaddcomlem  43277  zaddcom  43278  cnreeu  43304  dffltz  43406  3cubeslem2  43456  3cubeslem3l  43457  3cubeslem3r  43458  jm2.19lem3  43758  jm2.25  43766  int-addassocd  44940  binomcxplemnotnn0  45106  sub2times  46032  fperiodmullem  46062  dvnmul  46697  wallispilem4  46822  wallispi2lem2  46826  stirlinglem6  46833  dirkerper  46850  dirkertrigeqlem1  46852  dirkertrigeqlem2  46853  dirkertrigeqlem3  46854  dirkercncflem1  46857  fourierdlem26  46887  fourierdlem35  46896  fourierdlem42  46903  fourierdlem51  46911  fourierdlem64  46924  fourierdlem111  46971  hoidmv1lelem2  47346  hoidmvlelem2  47350  smflimlem4  47528  deccarry  48088  sqrtpwpw2p  48330  fmtnorec2lem  48334  fmtnorec3  48340  fmtnorec4  48341  mod42tp1mod8  48394  gpg5nbgrvtx13starlem2  48877  itcovalpclem2  49491  ackval1  49501  ackval2  49502  itscnhlc0yqe  49579  itsclquadb  49596  sinhpcosh  50558  crossp3i  50689