Theorem addassd 11154

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029

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

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

This theorem is referenced by:  addrid  11313  cnegex  11314  addlid  11316  addcan  11317  addcan2  11318  addcom  11319  addcomd  11335  muladd11r  11346  negeu  11370  addsubass  11390  nppcan3  11405  addsubsub23  11545  muladd  11569  add1p1  12392  div4p1lem1div2  12396  zpnn0elfzo1  13655  flhalf  13750  fldiv  13780  binom3  14147  bernneq  14152  discr1  14162  ccatass  14512  cshweqrep  14744  01sqrexlem7  15171  sqreulem  15283  isercoll2  15592  caucvgrlem  15596  iseraltlem2  15606  bcxmas  15758  bpoly4  15982  efsep  16035  efi4p  16062  efival  16077  pwp1fsum  16318  flodddiv4  16342  sadadd2lem2  16377  sadadd2lem  16386  sadasslem  16397  pcadd2  16818  prmreclem6  16849  4sqlem11  16883  vdwapun  16902  vdwlem3  16911  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  prmgaplem8  16986  psgnunilem2  19424  sylow1lem1  19527  efgredlemc  19674  psdmul  22109  opnreen  24776  ovolunlem1a  25453  nulmbl2  25493  unmbl  25494  volinun  25503  uniioombllem5  25544  itgcnlem  25747  ditgsplit  25818  dvnadd  25887  dvntaylp  26335  ulmshft  26355  ulmcn  26364  tangtx  26470  heron  26804  quad2  26805  dcubic1lem  26809  mcubic  26813  binom4  26816  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1  26822  quart  26827  lgamcvg2  27021  basellem2  27048  basellem3  27049  basellem8  27054  ppiub  27171  bcp1ctr  27246  bposlem9  27259  2lgslem3c  27365  2lgslem3d  27366  selberg3  27526  pntpbnd2  27554  pntibndlem2  27558  pntlemg  27565  pntlemk  27573  pntlemo  27574  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  finsumvtxdg2ssteplem4  29622  wwlksnextwrd  29970  wwlksnextproplem3  29984  wwlksext2clwwlk  30132  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  smcnlem  30772  stadd3i  32323  golem1  32346  quad3d  32829  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2  33215  archirngz  33271  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  subfacval2  35381  subfaclim  35382  subfacval3  35383  faclimlem1  35937  faclim2  35942  fwddifnp1  36359  dnizphlfeqhlf  36676  dnibndlem10  36687  dnibndlem13  36690  poimirlem16  37833  itg2addnclem3  37870  itg2addnc  37871  areacirclem1  37905  aks4d1p1p2  42320  posbezout  42350  2np3bcnp1  42394  sticksstones12a  42407  bcle2d  42429  aks6d1c7lem1  42430  readdridaddlidd  42509  nnadd1com  42518  nnaddcom  42519  nnadddir  42521  resubeulem1  42626  resubeulem2  42627  readdsub  42635  resubsub4  42640  resubidaddlidlem  42645  sn-addlid  42655  renegneg  42663  readdcan2  42664  renegid2  42665  sn-it0e0  42667  sn-negex12  42668  sn-addcand  42671  sn-addrid  42672  sn-addcan2d  42673  sn-subeu  42678  sn-0tie0  42702  zaddcomlem  42714  zaddcom  42715  cnreeu  42741  dffltz  42873  3cubeslem2  42923  3cubeslem3l  42924  3cubeslem3r  42925  jm2.19lem3  43229  jm2.25  43237  int-addassocd  44411  binomcxplemnotnn0  44593  sub2times  45517  fperiodmullem  45547  dvnmul  46183  wallispilem4  46308  wallispi2lem2  46312  stirlinglem6  46319  dirkerper  46336  dirkertrigeqlem1  46338  dirkertrigeqlem2  46339  dirkertrigeqlem3  46340  dirkercncflem1  46343  fourierdlem26  46373  fourierdlem35  46382  fourierdlem42  46389  fourierdlem51  46397  fourierdlem64  46410  fourierdlem111  46457  hoidmv1lelem2  46832  hoidmvlelem2  46836  smflimlem4  47014  deccarry  47553  sqrtpwpw2p  47780  fmtnorec2lem  47784  fmtnorec3  47790  fmtnorec4  47791  mod42tp1mod8  47844  gpg5nbgrvtx13starlem2  48314  itcovalpclem2  48913  ackval1  48923  ackval2  48924  itscnhlc0yqe  49001  itsclquadb  49018  sinhpcosh  49981