Theorem addassd 10461

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

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  (class class class)co 6975  ℂcc 10332   + caddc 10337

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-3an 1071

This theorem is referenced by:  addid1  10619  cnegex  10620  addid2  10622  addcan  10623  addcan2  10624  addcom  10625  addcomd  10641  muladd11r  10652  negeu  10675  addsubass  10696  nppcan3  10710  muladd  10872  add1p1  11697  div4p1lem1div2  11701  zpnn0elfzo1  12925  flhalf  13014  fldiv  13042  binom3  13399  bernneq  13404  discr1  13414  ccatass  13750  cshweqrep  14044  sqrlem7  14468  sqreulem  14579  isercoll2  14885  caucvgrlem  14889  iseraltlem2  14899  bcxmas  15049  bpoly4  15272  efsep  15322  efi4p  15349  efival  15364  pwp1fsum  15601  flodddiv4  15623  sadadd2lem2  15658  sadadd2lem  15667  sadasslem  15678  pcadd2  16081  prmreclem6  16112  4sqlem11  16146  vdwapun  16165  vdwlem3  16174  vdwlem6  16177  vdwlem8  16179  vdwlem9  16180  prmgaplem8  16249  psgnunilem2  18398  sylow1lem1  18497  efgredlemc  18643  opnreen  23158  ovolunlem1a  23816  nulmbl2  23856  unmbl  23857  volinun  23866  uniioombllem5  23907  itgcnlem  24109  ditgsplit  24178  dvnadd  24245  dvntaylp  24678  ulmshft  24697  ulmcn  24706  tangtx  24810  heron  25133  quad2  25134  dcubic1lem  25138  mcubic  25142  binom4  25145  dquartlem1  25146  dquartlem2  25147  dquart  25148  quart1  25151  quart  25156  lgamcvg2  25350  basellem2  25377  basellem3  25378  basellem8  25383  ppiub  25498  bcp1ctr  25573  bposlem9  25586  2lgslem3c  25692  2lgslem3d  25693  selberg3  25853  pntpbnd2  25881  pntibndlem2  25885  pntlemg  25892  pntlemk  25900  pntlemo  25901  axeuclidlem  26467  axcontlem2  26470  axcontlem4  26472  axcontlem7  26475  finsumvtxdg2ssteplem4  27049  wwlksnextwrd  27404  wwlksnextwrdOLD  27409  wwlksnextproplem3  27429  wwlksnextproplem3OLD  27430  wwlksext2clwwlk  27596  numclwlk2lem2f  27946  numclwlk2lem2f1o  27948  numclwlk2lem2fOLD  27949  numclwlk2lem2f1oOLD  27951  smcnlem  28267  stadd3i  29822  golem1  29845  archirngz  30517  subfacval2  32052  subfaclim  32053  subfacval3  32054  faclimlem1  32528  faclim2  32533  fwddifnp1  33180  dnizphlfeqhlf  33368  dnibndlem10  33379  dnibndlem13  33382  poimirlem16  34382  itg2addnclem3  34419  itg2addnc  34420  areacirclem1  34456  nnadd1com  38629  nnaddcom  38630  readdid2addid1d  38670  resubeulem1  38672  resubeulem2  38673  readdsub  38681  resubsub4  38684  resubidaddid1lem  38689  dffltz  38712  jm2.19lem3  39018  jm2.25  39026  int-addassocd  39926  binomcxplemnotnn0  40138  sub2times  40999  fperiodmullem  41029  dvnmul  41688  wallispilem4  41814  wallispi2lem2  41818  stirlinglem6  41825  dirkerper  41842  dirkertrigeqlem1  41844  dirkertrigeqlem2  41845  dirkertrigeqlem3  41846  dirkercncflem1  41849  fourierdlem26  41879  fourierdlem35  41888  fourierdlem42  41895  fourierdlem51  41903  fourierdlem64  41916  fourierdlem111  41963  hoidmv1lelem2  42335  hoidmvlelem2  42339  smflimlem4  42511  deccarry  42947  sqrtpwpw2p  43098  fmtnorec2lem  43102  fmtnorec3  43108  fmtnorec4  43109  mod42tp1mod8  43165  itscnhlc0yqe  44144  itsclquadb  44161  sinhpcosh  44236