Theorem addassd 11043

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   + caddc 10920

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1089

This theorem is referenced by:  addid1  11201  cnegex  11202  addid2  11204  addcan  11205  addcan2  11206  addcom  11207  addcomd  11223  muladd11r  11234  negeu  11257  addsubass  11277  nppcan3  11291  muladd  11453  add1p1  12270  div4p1lem1div2  12274  zpnn0elfzo1  13507  flhalf  13596  fldiv  13626  binom3  13985  bernneq  13990  discr1  14000  ccatass  14338  cshweqrep  14579  sqrlem7  15005  sqreulem  15116  isercoll2  15425  caucvgrlem  15429  iseraltlem2  15439  bcxmas  15592  bpoly4  15814  efsep  15864  efi4p  15891  efival  15906  pwp1fsum  16145  flodddiv4  16167  sadadd2lem2  16202  sadadd2lem  16211  sadasslem  16222  pcadd2  16636  prmreclem6  16667  4sqlem11  16701  vdwapun  16720  vdwlem3  16729  vdwlem6  16732  vdwlem8  16734  vdwlem9  16735  prmgaplem8  16804  psgnunilem2  19148  sylow1lem1  19248  efgredlemc  19396  opnreen  24039  ovolunlem1a  24705  nulmbl2  24745  unmbl  24746  volinun  24755  uniioombllem5  24796  itgcnlem  24999  ditgsplit  25070  dvnadd  25138  dvntaylp  25575  ulmshft  25594  ulmcn  25603  tangtx  25707  heron  26033  quad2  26034  dcubic1lem  26038  mcubic  26042  binom4  26045  dquartlem1  26046  dquartlem2  26047  dquart  26048  quart1  26051  quart  26056  lgamcvg2  26249  basellem2  26276  basellem3  26277  basellem8  26282  ppiub  26397  bcp1ctr  26472  bposlem9  26485  2lgslem3c  26591  2lgslem3d  26592  selberg3  26752  pntpbnd2  26780  pntibndlem2  26784  pntlemg  26791  pntlemk  26799  pntlemo  26800  axeuclidlem  27375  axcontlem2  27378  axcontlem4  27380  axcontlem7  27383  finsumvtxdg2ssteplem4  27960  wwlksnextwrd  28307  wwlksnextproplem3  28321  wwlksext2clwwlk  28466  numclwlk2lem2f  28786  numclwlk2lem2f1o  28788  smcnlem  29104  stadd3i  30655  golem1  30678  cycpmco2lem3  31440  cycpmco2lem4  31441  cycpmco2lem5  31442  cycpmco2lem6  31443  cycpmco2  31445  archirngz  31488  subfacval2  33194  subfaclim  33195  subfacval3  33196  faclimlem1  33754  faclim2  33759  fwddifnp1  34512  dnizphlfeqhlf  34701  dnibndlem10  34712  dnibndlem13  34715  poimirlem16  35837  itg2addnclem3  35874  itg2addnc  35875  areacirclem1  35909  aks4d1p1p2  40120  2np3bcnp1  40142  sticksstones12a  40155  2xp3dxp2ge1d  40204  readdid1addid2d  40331  nnadd1com  40334  nnaddcom  40335  nnadddir  40337  resubeulem1  40395  resubeulem2  40396  readdsub  40404  resubsub4  40409  resubidaddid1lem  40414  sn-addid2  40424  renegneg  40431  readdcan2  40432  renegid2  40433  sn-it0e0  40434  sn-negex12  40435  sn-addcand  40438  sn-addid1  40439  sn-addcan2d  40440  sn-subeu  40445  sn-0tie0  40458  cnreeu  40475  dffltz  40508  3cubeslem2  40544  3cubeslem3l  40545  3cubeslem3r  40546  jm2.19lem3  40851  jm2.25  40859  int-addassocd  41823  binomcxplemnotnn0  42012  sub2times  42861  fperiodmullem  42890  dvnmul  43533  wallispilem4  43658  wallispi2lem2  43662  stirlinglem6  43669  dirkerper  43686  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkertrigeqlem3  43690  dirkercncflem1  43693  fourierdlem26  43723  fourierdlem35  43732  fourierdlem42  43739  fourierdlem51  43747  fourierdlem64  43760  fourierdlem111  43807  hoidmv1lelem2  44180  hoidmvlelem2  44184  smflimlem4  44362  deccarry  44861  sqrtpwpw2p  45048  fmtnorec2lem  45052  fmtnorec3  45058  fmtnorec4  45059  mod42tp1mod8  45112  itcovalpclem2  46075  ackval1  46085  ackval2  46086  itscnhlc0yqe  46163  itsclquadb  46180  sinhpcosh  46500