Theorem addassd 10820

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692   + caddc 10697

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091

This theorem is referenced by:  addid1  10977  cnegex  10978  addid2  10980  addcan  10981  addcan2  10982  addcom  10983  addcomd  10999  muladd11r  11010  negeu  11033  addsubass  11053  nppcan3  11067  muladd  11229  add1p1  12046  div4p1lem1div2  12050  zpnn0elfzo1  13281  flhalf  13370  fldiv  13398  binom3  13756  bernneq  13761  discr1  13771  ccatass  14110  cshweqrep  14351  sqrlem7  14777  sqreulem  14888  isercoll2  15197  caucvgrlem  15201  iseraltlem2  15211  bcxmas  15362  bpoly4  15584  efsep  15634  efi4p  15661  efival  15676  pwp1fsum  15915  flodddiv4  15937  sadadd2lem2  15972  sadadd2lem  15981  sadasslem  15992  pcadd2  16406  prmreclem6  16437  4sqlem11  16471  vdwapun  16490  vdwlem3  16499  vdwlem6  16502  vdwlem8  16504  vdwlem9  16505  prmgaplem8  16574  psgnunilem2  18841  sylow1lem1  18941  efgredlemc  19089  opnreen  23682  ovolunlem1a  24347  nulmbl2  24387  unmbl  24388  volinun  24397  uniioombllem5  24438  itgcnlem  24641  ditgsplit  24712  dvnadd  24780  dvntaylp  25217  ulmshft  25236  ulmcn  25245  tangtx  25349  heron  25675  quad2  25676  dcubic1lem  25680  mcubic  25684  binom4  25687  dquartlem1  25688  dquartlem2  25689  dquart  25690  quart1  25693  quart  25698  lgamcvg2  25891  basellem2  25918  basellem3  25919  basellem8  25924  ppiub  26039  bcp1ctr  26114  bposlem9  26127  2lgslem3c  26233  2lgslem3d  26234  selberg3  26394  pntpbnd2  26422  pntibndlem2  26426  pntlemg  26433  pntlemk  26441  pntlemo  26442  axeuclidlem  27007  axcontlem2  27010  axcontlem4  27012  axcontlem7  27015  finsumvtxdg2ssteplem4  27590  wwlksnextwrd  27935  wwlksnextproplem3  27949  wwlksext2clwwlk  28094  numclwlk2lem2f  28414  numclwlk2lem2f1o  28416  smcnlem  28732  stadd3i  30283  golem1  30306  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2  31073  archirngz  31116  subfacval2  32816  subfaclim  32817  subfacval3  32818  faclimlem1  33378  faclim2  33383  fwddifnp1  34153  dnizphlfeqhlf  34342  dnibndlem10  34353  dnibndlem13  34356  poimirlem16  35479  itg2addnclem3  35516  itg2addnc  35517  areacirclem1  35551  aks4d1p1p2  39760  2np3bcnp1  39769  sticksstones12a  39782  2xp3dxp2ge1d  39825  readdid1addid2d  39942  nnadd1com  39945  nnaddcom  39946  nnadddir  39948  resubeulem1  40007  resubeulem2  40008  readdsub  40016  resubsub4  40021  resubidaddid1lem  40026  sn-addid2  40036  renegneg  40043  readdcan2  40044  renegid2  40045  sn-it0e0  40046  sn-negex12  40047  sn-addcand  40050  sn-addid1  40051  sn-addcan2d  40052  sn-subeu  40057  sn-0tie0  40070  cnreeu  40087  dffltz  40115  3cubeslem2  40151  3cubeslem3l  40152  3cubeslem3r  40153  jm2.19lem3  40457  jm2.25  40465  int-addassocd  41404  binomcxplemnotnn0  41588  sub2times  42426  fperiodmullem  42456  dvnmul  43102  wallispilem4  43227  wallispi2lem2  43231  stirlinglem6  43238  dirkerper  43255  dirkertrigeqlem1  43257  dirkertrigeqlem2  43258  dirkertrigeqlem3  43259  dirkercncflem1  43262  fourierdlem26  43292  fourierdlem35  43301  fourierdlem42  43308  fourierdlem51  43316  fourierdlem64  43329  fourierdlem111  43376  hoidmv1lelem2  43748  hoidmvlelem2  43752  smflimlem4  43924  deccarry  44419  sqrtpwpw2p  44606  fmtnorec2lem  44610  fmtnorec3  44616  fmtnorec4  44617  mod42tp1mod8  44670  itcovalpclem2  45633  ackval1  45643  ackval2  45644  itscnhlc0yqe  45721  itsclquadb  45738  sinhpcosh  46056