Theorem addassd 11165

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  addrid  11324  cnegex  11325  addlid  11327  addcan  11328  addcan2  11329  addcom  11330  addcomd  11346  muladd11r  11357  negeu  11381  addsubass  11401  nppcan3  11416  addsubsub23  11556  muladd  11580  nnadd1com  12198  nnaddcom  12199  nnadddir  12231  add1p1  12426  div4p1lem1div2  12430  zpnn0elfzo1  13692  flhalf  13787  fldiv  13817  binom3  14184  bernneq  14189  discr1  14199  ccatass  14549  cshweqrep  14781  01sqrexlem7  15208  sqreulem  15320  isercoll2  15629  caucvgrlem  15633  iseraltlem2  15643  bcxmas  15798  bpoly4  16022  efsep  16075  efi4p  16102  efival  16117  pwp1fsum  16358  flodddiv4  16382  sadadd2lem2  16417  sadadd2lem  16426  sadasslem  16437  pcadd2  16859  prmreclem6  16890  4sqlem11  16924  vdwapun  16943  vdwlem3  16952  vdwlem6  16955  vdwlem8  16957  vdwlem9  16958  prmgaplem8  17027  psgnunilem2  19468  sylow1lem1  19571  efgredlemc  19718  psdmul  22161  opnreen  24822  ovolunlem1a  25488  nulmbl2  25528  unmbl  25529  volinun  25538  uniioombllem5  25579  itgcnlem  25782  ditgsplit  25853  dvnadd  25921  dvntaylp  26361  ulmshft  26380  ulmcn  26389  tangtx  26494  heron  26827  quad2  26828  dcubic1lem  26832  mcubic  26836  binom4  26839  dquartlem1  26840  dquartlem2  26841  dquart  26842  quart1  26845  quart  26850  lgamcvg2  27043  basellem2  27070  basellem3  27071  basellem8  27076  ppiub  27192  bcp1ctr  27267  bposlem9  27280  2lgslem3c  27386  2lgslem3d  27387  selberg3  27547  pntpbnd2  27575  pntibndlem2  27579  pntlemg  27586  pntlemk  27594  pntlemo  27595  axeuclidlem  29056  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  finsumvtxdg2ssteplem4  29642  wwlksnextwrd  29990  wwlksnextproplem3  30004  wwlksext2clwwlk  30152  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  smcnlem  30793  stadd3i  32344  golem1  32367  quad3d  32848  cycpmco2lem3  33216  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2  33221  archirngz  33277  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  subfacval2  35422  subfaclim  35423  subfacval3  35424  faclimlem1  35978  faclim2  35983  fwddifnp1  36400  dnizphlfeqhlf  36789  dnibndlem10  36800  dnibndlem13  36803  qdiff  37694  poimirlem16  38010  itg2addnclem3  38047  itg2addnc  38048  areacirclem1  38082  aks4d1p1p2  42562  posbezout  42592  2np3bcnp1  42636  sticksstones12a  42649  bcle2d  42671  aks6d1c7lem1  42672  readdridaddlidd  42748  resubeulem1  42859  resubeulem2  42860  readdsub  42868  resubsub4  42873  resubidaddlidlem  42878  sn-addlid  42888  renegneg  42896  readdcan2  42897  renegid2  42898  sn-it0e0  42900  sn-negex12  42901  sn-addcand  42904  sn-addrid  42905  sn-addcan2d  42906  sn-subeu  42911  sn-0tie0  42948  zaddcomlem  42960  zaddcom  42961  cnreeu  42987  dffltz  43091  3cubeslem2  43141  3cubeslem3l  43142  3cubeslem3r  43143  jm2.19lem3  43443  jm2.25  43451  int-addassocd  44625  binomcxplemnotnn0  44807  sub2times  45728  fperiodmullem  45758  dvnmul  46393  wallispilem4  46518  wallispi2lem2  46522  stirlinglem6  46529  dirkerper  46546  dirkertrigeqlem1  46548  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  dirkercncflem1  46553  fourierdlem26  46583  fourierdlem35  46592  fourierdlem42  46599  fourierdlem51  46607  fourierdlem64  46620  fourierdlem111  46667  hoidmv1lelem2  47042  hoidmvlelem2  47046  smflimlem4  47224  deccarry  47781  sqrtpwpw2p  48023  fmtnorec2lem  48027  fmtnorec3  48033  fmtnorec4  48034  mod42tp1mod8  48087  gpg5nbgrvtx13starlem2  48570  itcovalpclem2  49169  ackval1  49179  ackval2  49180  itscnhlc0yqe  49257  itsclquadb  49274  sinhpcosh  50237