Theorem addassd 11141

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016

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

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

This theorem is referenced by:  addrid  11300  cnegex  11301  addlid  11303  addcan  11304  addcan2  11305  addcom  11306  addcomd  11322  muladd11r  11333  negeu  11357  addsubass  11377  nppcan3  11392  addsubsub23  11532  muladd  11556  add1p1  12379  div4p1lem1div2  12383  zpnn0elfzo1  13641  flhalf  13736  fldiv  13766  binom3  14133  bernneq  14138  discr1  14148  ccatass  14498  cshweqrep  14730  01sqrexlem7  15157  sqreulem  15269  isercoll2  15578  caucvgrlem  15582  iseraltlem2  15592  bcxmas  15744  bpoly4  15968  efsep  16021  efi4p  16048  efival  16063  pwp1fsum  16304  flodddiv4  16328  sadadd2lem2  16363  sadadd2lem  16372  sadasslem  16383  pcadd2  16804  prmreclem6  16835  4sqlem11  16869  vdwapun  16888  vdwlem3  16897  vdwlem6  16900  vdwlem8  16902  vdwlem9  16903  prmgaplem8  16972  psgnunilem2  19409  sylow1lem1  19512  efgredlemc  19659  psdmul  22082  opnreen  24748  ovolunlem1a  25425  nulmbl2  25465  unmbl  25466  volinun  25475  uniioombllem5  25516  itgcnlem  25719  ditgsplit  25790  dvnadd  25859  dvntaylp  26307  ulmshft  26327  ulmcn  26336  tangtx  26442  heron  26776  quad2  26777  dcubic1lem  26781  mcubic  26785  binom4  26788  dquartlem1  26789  dquartlem2  26790  dquart  26791  quart1  26794  quart  26799  lgamcvg2  26993  basellem2  27020  basellem3  27021  basellem8  27026  ppiub  27143  bcp1ctr  27218  bposlem9  27231  2lgslem3c  27337  2lgslem3d  27338  selberg3  27498  pntpbnd2  27526  pntibndlem2  27530  pntlemg  27537  pntlemk  27545  pntlemo  27546  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  finsumvtxdg2ssteplem4  29529  wwlksnextwrd  29877  wwlksnextproplem3  29891  wwlksext2clwwlk  30039  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  smcnlem  30679  stadd3i  32230  golem1  32253  quad3d  32737  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2  33109  archirngz  33165  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  subfacval2  35252  subfaclim  35253  subfacval3  35254  faclimlem1  35808  faclim2  35813  fwddifnp1  36230  dnizphlfeqhlf  36541  dnibndlem10  36552  dnibndlem13  36555  poimirlem16  37696  itg2addnclem3  37733  itg2addnc  37734  areacirclem1  37768  aks4d1p1p2  42183  posbezout  42213  2np3bcnp1  42257  sticksstones12a  42270  bcle2d  42292  aks6d1c7lem1  42293  readdridaddlidd  42376  nnadd1com  42385  nnaddcom  42386  nnadddir  42388  resubeulem1  42493  resubeulem2  42494  readdsub  42502  resubsub4  42507  resubidaddlidlem  42512  sn-addlid  42522  renegneg  42530  readdcan2  42531  renegid2  42532  sn-it0e0  42534  sn-negex12  42535  sn-addcand  42538  sn-addrid  42539  sn-addcan2d  42540  sn-subeu  42545  sn-0tie0  42569  zaddcomlem  42581  zaddcom  42582  cnreeu  42608  dffltz  42752  3cubeslem2  42802  3cubeslem3l  42803  3cubeslem3r  42804  jm2.19lem3  43108  jm2.25  43116  int-addassocd  44291  binomcxplemnotnn0  44473  sub2times  45398  fperiodmullem  45428  dvnmul  46065  wallispilem4  46190  wallispi2lem2  46194  stirlinglem6  46201  dirkerper  46218  dirkertrigeqlem1  46220  dirkertrigeqlem2  46221  dirkertrigeqlem3  46222  dirkercncflem1  46225  fourierdlem26  46255  fourierdlem35  46264  fourierdlem42  46271  fourierdlem51  46279  fourierdlem64  46292  fourierdlem111  46339  hoidmv1lelem2  46714  hoidmvlelem2  46718  smflimlem4  46896  deccarry  47435  sqrtpwpw2p  47662  fmtnorec2lem  47666  fmtnorec3  47672  fmtnorec4  47673  mod42tp1mod8  47726  gpg5nbgrvtx13starlem2  48196  itcovalpclem2  48796  ackval1  48806  ackval2  48807  itscnhlc0yqe  48884  itsclquadb  48901  sinhpcosh  49865