Theorem addassd 11257

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   + caddc 11132

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

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

This theorem is referenced by:  addrid  11415  cnegex  11416  addlid  11418  addcan  11419  addcan2  11420  addcom  11421  addcomd  11437  muladd11r  11448  negeu  11472  addsubass  11492  nppcan3  11507  muladd  11669  add1p1  12492  div4p1lem1div2  12496  zpnn0elfzo1  13755  flhalf  13847  fldiv  13877  binom3  14242  bernneq  14247  discr1  14257  ccatass  14606  cshweqrep  14839  01sqrexlem7  15267  sqreulem  15378  isercoll2  15685  caucvgrlem  15689  iseraltlem2  15699  bcxmas  15851  bpoly4  16075  efsep  16128  efi4p  16155  efival  16170  pwp1fsum  16410  flodddiv4  16434  sadadd2lem2  16469  sadadd2lem  16478  sadasslem  16489  pcadd2  16910  prmreclem6  16941  4sqlem11  16975  vdwapun  16994  vdwlem3  17003  vdwlem6  17006  vdwlem8  17008  vdwlem9  17009  prmgaplem8  17078  psgnunilem2  19476  sylow1lem1  19579  efgredlemc  19726  psdmul  22104  opnreen  24771  ovolunlem1a  25449  nulmbl2  25489  unmbl  25490  volinun  25499  uniioombllem5  25540  itgcnlem  25743  ditgsplit  25814  dvnadd  25883  dvntaylp  26331  ulmshft  26351  ulmcn  26360  tangtx  26466  heron  26800  quad2  26801  dcubic1lem  26805  mcubic  26809  binom4  26812  dquartlem1  26813  dquartlem2  26814  dquart  26815  quart1  26818  quart  26823  lgamcvg2  27017  basellem2  27044  basellem3  27045  basellem8  27050  ppiub  27167  bcp1ctr  27242  bposlem9  27255  2lgslem3c  27361  2lgslem3d  27362  selberg3  27522  pntpbnd2  27550  pntibndlem2  27554  pntlemg  27561  pntlemk  27569  pntlemo  27570  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  finsumvtxdg2ssteplem4  29528  wwlksnextwrd  29879  wwlksnextproplem3  29893  wwlksext2clwwlk  30038  numclwlk2lem2f  30358  numclwlk2lem2f1o  30360  smcnlem  30678  stadd3i  32229  golem1  32252  quad3d  32727  cycpmco2lem3  33139  cycpmco2lem4  33140  cycpmco2lem5  33141  cycpmco2lem6  33142  cycpmco2  33144  archirngz  33187  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  subfacval2  35209  subfaclim  35210  subfacval3  35211  faclimlem1  35760  faclim2  35765  fwddifnp1  36183  dnizphlfeqhlf  36494  dnibndlem10  36505  dnibndlem13  36508  poimirlem16  37660  itg2addnclem3  37697  itg2addnc  37698  areacirclem1  37732  aks4d1p1p2  42083  posbezout  42113  2np3bcnp1  42157  sticksstones12a  42170  bcle2d  42192  aks6d1c7lem1  42193  2xp3dxp2ge1d  42254  readdridaddlidd  42309  nnadd1com  42317  nnaddcom  42318  nnadddir  42320  resubeulem1  42418  resubeulem2  42419  readdsub  42427  resubsub4  42432  resubidaddlidlem  42437  sn-addlid  42447  renegneg  42454  readdcan2  42455  renegid2  42456  sn-it0e0  42458  sn-negex12  42459  sn-addcand  42462  sn-addrid  42463  sn-addcan2d  42464  sn-subeu  42469  sn-0tie0  42482  zaddcomlem  42494  zaddcom  42495  cnreeu  42513  dffltz  42657  3cubeslem2  42708  3cubeslem3l  42709  3cubeslem3r  42710  jm2.19lem3  43015  jm2.25  43023  int-addassocd  44198  binomcxplemnotnn0  44380  sub2times  45301  fperiodmullem  45332  dvnmul  45972  wallispilem4  46097  wallispi2lem2  46101  stirlinglem6  46108  dirkerper  46125  dirkertrigeqlem1  46127  dirkertrigeqlem2  46128  dirkertrigeqlem3  46129  dirkercncflem1  46132  fourierdlem26  46162  fourierdlem35  46171  fourierdlem42  46178  fourierdlem51  46186  fourierdlem64  46199  fourierdlem111  46246  hoidmv1lelem2  46621  hoidmvlelem2  46625  smflimlem4  46803  deccarry  47340  sqrtpwpw2p  47552  fmtnorec2lem  47556  fmtnorec3  47562  fmtnorec4  47563  mod42tp1mod8  47616  gpg5nbgrvtx13starlem2  48074  itcovalpclem2  48651  ackval1  48661  ackval2  48662  itscnhlc0yqe  48739  itsclquadb  48756  sinhpcosh  49604