Theorem addassd 11232

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  addrid  11391  cnegex  11392  addlid  11394  addcan  11395  addcan2  11396  addcom  11397  addcomd  11413  muladd11r  11424  negeu  11448  addsubass  11468  nppcan3  11483  addsubsub23  11623  muladd  11647  nnadd1com  12260  nnaddcom  12261  nnadddir  12293  add1p1  12496  div4p1lem1div2  12500  zpnn0elfzo1  13770  flhalf  13865  fldiv  13895  binom3  14262  bernneq  14267  discr1  14277  ccatass  14628  cshweqrep  14860  01sqrexlem7  15301  sqreulem  15413  isercoll2  15722  caucvgrlem  15726  iseraltlem2  15736  bcxmas  15891  bpoly4  16114  efsep  16167  efi4p  16194  efival  16209  pwp1fsum  16450  flodddiv4  16474  sadadd2lem2  16509  sadadd2lem  16518  sadasslem  16529  pcadd2  16951  prmreclem6  16982  4sqlem11  17016  vdwapun  17035  vdwlem3  17044  vdwlem6  17047  vdwlem8  17049  vdwlem9  17050  prmgaplem8  17119  psgnunilem2  19566  sylow1lem1  19669  efgredlemc  19816  psdmul  22310  opnreen  24970  ovolunlem1a  25636  nulmbl2  25676  unmbl  25677  volinun  25686  uniioombllem5  25727  itgcnlem  25930  ditgsplit  26001  dvnadd  26069  dvntaylp  26512  ulmshft  26531  ulmcn  26540  tangtx  26648  heron  26981  quad2  26982  dcubic1lem  26986  mcubic  26990  binom4  26993  dquartlem1  26994  dquartlem2  26995  dquart  26996  quart1  26999  quart  27004  lgamcvg2  27197  basellem2  27224  basellem3  27225  basellem8  27230  ppiub  27346  bcp1ctr  27421  bposlem9  27434  2lgslem3c  27540  2lgslem3d  27541  selberg3  27701  pntpbnd2  27729  pntibndlem2  27733  pntlemg  27740  pntlemk  27748  pntlemo  27749  axeuclidlem  29290  axcontlem2  29293  axcontlem4  29295  axcontlem7  29298  finsumvtxdg2ssteplem4  29876  wwlksnextwrd  30224  wwlksnextproplem3  30238  wwlksext2clwwlk  30386  numclwlk2lem2f  30706  numclwlk2lem2f1o  30708  smcnlem  31027  stadd3i  32578  golem1  32601  quad3d  33072  cycpmco2lem3  33426  cycpmco2lem4  33427  cycpmco2lem5  33428  cycpmco2lem6  33429  cycpmco2  33431  archirngz  33487  constrrtlc1  34100  constrrtcclem  34102  constrrtcc  34103  cos9thpiminplylem1  34150  cos9thpiminplylem2  34151  subfacval2  35657  subfaclim  35658  subfacval3  35659  faclimlem1  36213  faclim2  36218  fwddifnp1  36635  dnizphlfeqhlf  37043  dnibndlem10  37054  dnibndlem13  37057  qdiff  37949  poimirlem16  38265  itg2addnclem3  38302  itg2addnc  38303  areacirclem1  38337  aks4d1p1p2  42815  posbezout  42845  2np3bcnp1  42889  sticksstones12a  42902  bcle2d  42924  aks6d1c7lem1  42925  quadfac  42950  readdridaddlidd  43003  resubeulem1  43114  resubeulem2  43115  readdsub  43123  resubsub4  43128  resubidaddlidlem  43133  sn-addlid  43143  renegneg  43151  readdcan2  43152  renegid2  43153  sn-it0e0  43155  sn-negex12  43156  sn-addcand  43159  sn-addrid  43160  sn-addcan2d  43161  sn-subeu  43166  sn-0tie0  43203  zaddcomlem  43215  zaddcom  43216  cnreeu  43242  dffltz  43346  3cubeslem2  43396  3cubeslem3l  43397  3cubeslem3r  43398  jm2.19lem3  43698  jm2.25  43706  int-addassocd  44880  binomcxplemnotnn0  45046  sub2times  45972  fperiodmullem  46002  dvnmul  46637  wallispilem4  46762  wallispi2lem2  46766  stirlinglem6  46773  dirkerper  46790  dirkertrigeqlem1  46792  dirkertrigeqlem2  46793  dirkertrigeqlem3  46794  dirkercncflem1  46797  fourierdlem26  46827  fourierdlem35  46836  fourierdlem42  46843  fourierdlem51  46851  fourierdlem64  46864  fourierdlem111  46911  hoidmv1lelem2  47286  hoidmvlelem2  47290  smflimlem4  47468  deccarry  48025  sqrtpwpw2p  48267  fmtnorec2lem  48271  fmtnorec3  48277  fmtnorec4  48278  mod42tp1mod8  48331  gpg5nbgrvtx13starlem2  48814  itcovalpclem2  49428  ackval1  49438  ackval2  49439  itscnhlc0yqe  49516  itsclquadb  49533  sinhpcosh  50495