Theorem addassd 11155

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025   + caddc 11030

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

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

This theorem is referenced by:  addrid  11314  cnegex  11315  addlid  11317  addcan  11318  addcan2  11319  addcom  11320  addcomd  11336  muladd11r  11347  negeu  11371  addsubass  11391  nppcan3  11406  addsubsub23  11546  muladd  11570  add1p1  12393  div4p1lem1div2  12397  zpnn0elfzo1  13656  flhalf  13751  fldiv  13781  binom3  14148  bernneq  14153  discr1  14163  ccatass  14513  cshweqrep  14745  01sqrexlem7  15172  sqreulem  15284  isercoll2  15593  caucvgrlem  15597  iseraltlem2  15607  bcxmas  15759  bpoly4  15983  efsep  16036  efi4p  16063  efival  16078  pwp1fsum  16319  flodddiv4  16343  sadadd2lem2  16378  sadadd2lem  16387  sadasslem  16398  pcadd2  16819  prmreclem6  16850  4sqlem11  16884  vdwapun  16903  vdwlem3  16912  vdwlem6  16915  vdwlem8  16917  vdwlem9  16918  prmgaplem8  16987  psgnunilem2  19428  sylow1lem1  19531  efgredlemc  19678  psdmul  22110  opnreen  24775  ovolunlem1a  25441  nulmbl2  25481  unmbl  25482  volinun  25491  uniioombllem5  25532  itgcnlem  25735  ditgsplit  25806  dvnadd  25874  dvntaylp  26319  ulmshft  26339  ulmcn  26348  tangtx  26454  heron  26788  quad2  26789  dcubic1lem  26793  mcubic  26797  binom4  26800  dquartlem1  26801  dquartlem2  26802  dquart  26803  quart1  26806  quart  26811  lgamcvg2  27005  basellem2  27032  basellem3  27033  basellem8  27038  ppiub  27155  bcp1ctr  27230  bposlem9  27243  2lgslem3c  27349  2lgslem3d  27350  selberg3  27510  pntpbnd2  27538  pntibndlem2  27542  pntlemg  27549  pntlemk  27557  pntlemo  27558  axeuclidlem  29019  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  finsumvtxdg2ssteplem4  29606  wwlksnextwrd  29954  wwlksnextproplem3  29968  wwlksext2clwwlk  30116  numclwlk2lem2f  30436  numclwlk2lem2f1o  30438  smcnlem  30757  stadd3i  32308  golem1  32331  quad3d  32812  cycpmco2lem3  33194  cycpmco2lem4  33195  cycpmco2lem5  33196  cycpmco2lem6  33197  cycpmco2  33199  archirngz  33255  constrrtlc1  33882  constrrtcclem  33884  constrrtcc  33885  cos9thpiminplylem1  33932  cos9thpiminplylem2  33933  subfacval2  35375  subfaclim  35376  subfacval3  35377  faclimlem1  35931  faclim2  35936  fwddifnp1  36353  dnizphlfeqhlf  36734  dnibndlem10  36745  dnibndlem13  36748  poimirlem16  37948  itg2addnclem3  37985  itg2addnc  37986  areacirclem1  38020  aks4d1p1p2  42501  posbezout  42531  2np3bcnp1  42575  sticksstones12a  42588  bcle2d  42610  aks6d1c7lem1  42611  readdridaddlidd  42689  nnadd1com  42698  nnaddcom  42699  nnadddir  42701  resubeulem1  42806  resubeulem2  42807  readdsub  42815  resubsub4  42820  resubidaddlidlem  42825  sn-addlid  42835  renegneg  42843  readdcan2  42844  renegid2  42845  sn-it0e0  42847  sn-negex12  42848  sn-addcand  42851  sn-addrid  42852  sn-addcan2d  42853  sn-subeu  42858  sn-0tie0  42895  zaddcomlem  42907  zaddcom  42908  cnreeu  42934  dffltz  43066  3cubeslem2  43116  3cubeslem3l  43117  3cubeslem3r  43118  jm2.19lem3  43422  jm2.25  43430  int-addassocd  44604  binomcxplemnotnn0  44786  sub2times  45709  fperiodmullem  45739  dvnmul  46375  wallispilem4  46500  wallispi2lem2  46504  stirlinglem6  46511  dirkerper  46528  dirkertrigeqlem1  46530  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  dirkercncflem1  46535  fourierdlem26  46565  fourierdlem35  46574  fourierdlem42  46581  fourierdlem51  46589  fourierdlem64  46602  fourierdlem111  46649  hoidmv1lelem2  47024  hoidmvlelem2  47028  smflimlem4  47206  deccarry  47745  sqrtpwpw2p  47972  fmtnorec2lem  47976  fmtnorec3  47982  fmtnorec4  47983  mod42tp1mod8  48036  gpg5nbgrvtx13starlem2  48506  itcovalpclem2  49105  ackval1  49115  ackval2  49116  itscnhlc0yqe  49193  itsclquadb  49210  sinhpcosh  50173