Theorem addassd 11312

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187

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

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

This theorem is referenced by:  addrid  11470  cnegex  11471  addlid  11473  addcan  11474  addcan2  11475  addcom  11476  addcomd  11492  muladd11r  11503  negeu  11526  addsubass  11546  nppcan3  11560  muladd  11722  add1p1  12544  div4p1lem1div2  12548  zpnn0elfzo1  13790  flhalf  13881  fldiv  13911  binom3  14273  bernneq  14278  discr1  14288  ccatass  14636  cshweqrep  14869  01sqrexlem7  15297  sqreulem  15408  isercoll2  15717  caucvgrlem  15721  iseraltlem2  15731  bcxmas  15883  bpoly4  16107  efsep  16158  efi4p  16185  efival  16200  pwp1fsum  16439  flodddiv4  16461  sadadd2lem2  16496  sadadd2lem  16505  sadasslem  16516  pcadd2  16937  prmreclem6  16968  4sqlem11  17002  vdwapun  17021  vdwlem3  17030  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  prmgaplem8  17105  psgnunilem2  19537  sylow1lem1  19640  efgredlemc  19787  psdmul  22193  opnreen  24872  ovolunlem1a  25550  nulmbl2  25590  unmbl  25591  volinun  25600  uniioombllem5  25641  itgcnlem  25845  ditgsplit  25916  dvnadd  25985  dvntaylp  26431  ulmshft  26451  ulmcn  26460  tangtx  26565  heron  26899  quad2  26900  dcubic1lem  26904  mcubic  26908  binom4  26911  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1  26917  quart  26922  lgamcvg2  27116  basellem2  27143  basellem3  27144  basellem8  27149  ppiub  27266  bcp1ctr  27341  bposlem9  27354  2lgslem3c  27460  2lgslem3d  27461  selberg3  27621  pntpbnd2  27649  pntibndlem2  27653  pntlemg  27660  pntlemk  27668  pntlemo  27669  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  finsumvtxdg2ssteplem4  29584  wwlksnextwrd  29930  wwlksnextproplem3  29944  wwlksext2clwwlk  30089  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  smcnlem  30729  stadd3i  32280  golem1  32303  quad3d  32757  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  archirngz  33169  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  subfacval2  35155  subfaclim  35156  subfacval3  35157  faclimlem1  35705  faclim2  35710  fwddifnp1  36129  dnizphlfeqhlf  36442  dnibndlem10  36453  dnibndlem13  36456  poimirlem16  37596  itg2addnclem3  37633  itg2addnc  37634  areacirclem1  37668  aks4d1p1p2  42027  posbezout  42057  2np3bcnp1  42101  sticksstones12a  42114  bcle2d  42136  aks6d1c7lem1  42137  2xp3dxp2ge1d  42198  readdridaddlidd  42253  nnadd1com  42256  nnaddcom  42257  nnadddir  42259  resubeulem1  42351  resubeulem2  42352  readdsub  42360  resubsub4  42365  resubidaddlidlem  42370  sn-addlid  42380  renegneg  42387  readdcan2  42388  renegid2  42389  sn-it0e0  42391  sn-negex12  42392  sn-addcand  42395  sn-addrid  42396  sn-addcan2d  42397  sn-subeu  42402  sn-0tie0  42415  zaddcomlem  42427  zaddcom  42428  cnreeu  42446  dffltz  42589  3cubeslem2  42641  3cubeslem3l  42642  3cubeslem3r  42643  jm2.19lem3  42948  jm2.25  42956  int-addassocd  44136  binomcxplemnotnn0  44325  sub2times  45187  fperiodmullem  45218  dvnmul  45864  wallispilem4  45989  wallispi2lem2  45993  stirlinglem6  46000  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkercncflem1  46024  fourierdlem26  46054  fourierdlem35  46063  fourierdlem42  46070  fourierdlem51  46078  fourierdlem64  46091  fourierdlem111  46138  hoidmv1lelem2  46513  hoidmvlelem2  46517  smflimlem4  46695  deccarry  47226  sqrtpwpw2p  47412  fmtnorec2lem  47416  fmtnorec3  47422  fmtnorec4  47423  mod42tp1mod8  47476  itcovalpclem2  48405  ackval1  48415  ackval2  48416  itscnhlc0yqe  48493  itsclquadb  48510  sinhpcosh  48832