Theorem addassd 10981

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   + caddc 10858

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  addid1  11138  cnegex  11139  addid2  11141  addcan  11142  addcan2  11143  addcom  11144  addcomd  11160  muladd11r  11171  negeu  11194  addsubass  11214  nppcan3  11228  muladd  11390  add1p1  12207  div4p1lem1div2  12211  zpnn0elfzo1  13442  flhalf  13531  fldiv  13561  binom3  13920  bernneq  13925  discr1  13935  ccatass  14274  cshweqrep  14515  sqrlem7  14941  sqreulem  15052  isercoll2  15361  caucvgrlem  15365  iseraltlem2  15375  bcxmas  15528  bpoly4  15750  efsep  15800  efi4p  15827  efival  15842  pwp1fsum  16081  flodddiv4  16103  sadadd2lem2  16138  sadadd2lem  16147  sadasslem  16158  pcadd2  16572  prmreclem6  16603  4sqlem11  16637  vdwapun  16656  vdwlem3  16665  vdwlem6  16668  vdwlem8  16670  vdwlem9  16671  prmgaplem8  16740  psgnunilem2  19084  sylow1lem1  19184  efgredlemc  19332  opnreen  23975  ovolunlem1a  24641  nulmbl2  24681  unmbl  24682  volinun  24691  uniioombllem5  24732  itgcnlem  24935  ditgsplit  25006  dvnadd  25074  dvntaylp  25511  ulmshft  25530  ulmcn  25539  tangtx  25643  heron  25969  quad2  25970  dcubic1lem  25974  mcubic  25978  binom4  25981  dquartlem1  25982  dquartlem2  25983  dquart  25984  quart1  25987  quart  25992  lgamcvg2  26185  basellem2  26212  basellem3  26213  basellem8  26218  ppiub  26333  bcp1ctr  26408  bposlem9  26421  2lgslem3c  26527  2lgslem3d  26528  selberg3  26688  pntpbnd2  26716  pntibndlem2  26720  pntlemg  26727  pntlemk  26735  pntlemo  26736  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  finsumvtxdg2ssteplem4  27896  wwlksnextwrd  28241  wwlksnextproplem3  28255  wwlksext2clwwlk  28400  numclwlk2lem2f  28720  numclwlk2lem2f1o  28722  smcnlem  29038  stadd3i  30589  golem1  30612  cycpmco2lem3  31374  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2  31379  archirngz  31422  subfacval2  33128  subfaclim  33129  subfacval3  33130  faclimlem1  33688  faclim2  33693  fwddifnp1  34446  dnizphlfeqhlf  34635  dnibndlem10  34646  dnibndlem13  34649  poimirlem16  35772  itg2addnclem3  35809  itg2addnc  35810  areacirclem1  35844  aks4d1p1p2  40058  2np3bcnp1  40080  sticksstones12a  40093  2xp3dxp2ge1d  40142  readdid1addid2d  40274  nnadd1com  40277  nnaddcom  40278  nnadddir  40280  resubeulem1  40338  resubeulem2  40339  readdsub  40347  resubsub4  40352  resubidaddid1lem  40357  sn-addid2  40367  renegneg  40374  readdcan2  40375  renegid2  40376  sn-it0e0  40377  sn-negex12  40378  sn-addcand  40381  sn-addid1  40382  sn-addcan2d  40383  sn-subeu  40388  sn-0tie0  40401  cnreeu  40418  dffltz  40451  3cubeslem2  40487  3cubeslem3l  40488  3cubeslem3r  40489  jm2.19lem3  40793  jm2.25  40801  int-addassocd  41738  binomcxplemnotnn0  41927  sub2times  42766  fperiodmullem  42796  dvnmul  43438  wallispilem4  43563  wallispi2lem2  43567  stirlinglem6  43574  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkertrigeqlem3  43595  dirkercncflem1  43598  fourierdlem26  43628  fourierdlem35  43637  fourierdlem42  43644  fourierdlem51  43652  fourierdlem64  43665  fourierdlem111  43712  hoidmv1lelem2  44084  hoidmvlelem2  44088  smflimlem4  44260  deccarry  44755  sqrtpwpw2p  44942  fmtnorec2lem  44946  fmtnorec3  44952  fmtnorec4  44953  mod42tp1mod8  45006  itcovalpclem2  45969  ackval1  45979  ackval2  45980  itscnhlc0yqe  46057  itsclquadb  46074  sinhpcosh  46394