Theorem addassd 10666

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  (class class class)co 7159  ℂcc 10538   + caddc 10543

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  addid1  10823  cnegex  10824  addid2  10826  addcan  10827  addcan2  10828  addcom  10829  addcomd  10845  muladd11r  10856  negeu  10879  addsubass  10899  nppcan3  10913  muladd  11075  add1p1  11891  div4p1lem1div2  11895  zpnn0elfzo1  13114  flhalf  13203  fldiv  13231  binom3  13588  bernneq  13593  discr1  13603  ccatass  13945  cshweqrep  14186  sqrlem7  14611  sqreulem  14722  isercoll2  15028  caucvgrlem  15032  iseraltlem2  15042  bcxmas  15193  bpoly4  15416  efsep  15466  efi4p  15493  efival  15508  pwp1fsum  15745  flodddiv4  15767  sadadd2lem2  15802  sadadd2lem  15811  sadasslem  15822  pcadd2  16229  prmreclem6  16260  4sqlem11  16294  vdwapun  16313  vdwlem3  16322  vdwlem6  16325  vdwlem8  16327  vdwlem9  16328  prmgaplem8  16397  psgnunilem2  18626  sylow1lem1  18726  efgredlemc  18874  opnreen  23442  ovolunlem1a  24100  nulmbl2  24140  unmbl  24141  volinun  24150  uniioombllem5  24191  itgcnlem  24393  ditgsplit  24462  dvnadd  24529  dvntaylp  24962  ulmshft  24981  ulmcn  24990  tangtx  25094  heron  25419  quad2  25420  dcubic1lem  25424  mcubic  25428  binom4  25431  dquartlem1  25432  dquartlem2  25433  dquart  25434  quart1  25437  quart  25442  lgamcvg2  25635  basellem2  25662  basellem3  25663  basellem8  25668  ppiub  25783  bcp1ctr  25858  bposlem9  25871  2lgslem3c  25977  2lgslem3d  25978  selberg3  26138  pntpbnd2  26166  pntibndlem2  26170  pntlemg  26177  pntlemk  26185  pntlemo  26186  axeuclidlem  26751  axcontlem2  26754  axcontlem4  26756  axcontlem7  26759  finsumvtxdg2ssteplem4  27333  wwlksnextwrd  27678  wwlksnextproplem3  27693  wwlksext2clwwlk  27839  numclwlk2lem2f  28159  numclwlk2lem2f1o  28161  smcnlem  28477  stadd3i  30028  golem1  30051  cycpmco2lem3  30774  cycpmco2lem4  30775  cycpmco2lem5  30776  cycpmco2lem6  30777  cycpmco2  30779  archirngz  30822  subfacval2  32438  subfaclim  32439  subfacval3  32440  faclimlem1  32979  faclim2  32984  fwddifnp1  33630  dnizphlfeqhlf  33819  dnibndlem10  33830  dnibndlem13  33833  poimirlem16  34912  itg2addnclem3  34949  itg2addnc  34950  areacirclem1  34986  readdid1addid2d  39163  nnadd1com  39166  nnaddcom  39167  nnadddir  39169  resubeulem1  39211  resubeulem2  39212  readdsub  39220  resubsub4  39225  resubidaddid1lem  39230  sn-addid2  39240  renegneg  39247  readdcan2  39248  dffltz  39277  3cubeslem2  39288  3cubeslem3l  39289  3cubeslem3r  39290  jm2.19lem3  39594  jm2.25  39602  int-addassocd  40533  binomcxplemnotnn0  40694  sub2times  41546  fperiodmullem  41576  dvnmul  42234  wallispilem4  42360  wallispi2lem2  42364  stirlinglem6  42371  dirkerper  42388  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkercncflem1  42395  fourierdlem26  42425  fourierdlem35  42434  fourierdlem42  42441  fourierdlem51  42449  fourierdlem64  42462  fourierdlem111  42509  hoidmv1lelem2  42881  hoidmvlelem2  42885  smflimlem4  43057  deccarry  43518  sqrtpwpw2p  43707  fmtnorec2lem  43711  fmtnorec3  43717  fmtnorec4  43718  mod42tp1mod8  43774  itscnhlc0yqe  44753  itsclquadb  44770  sinhpcosh  44846