Theorem addassd 11331

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198   + caddc 11203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11265

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11490  cnegex  11491  addlid  11493  addcan  11494  addcan2  11495  addcom  11496  addcomd  11512  muladd11r  11523  negeu  11547  addsubass  11567  nppcan3  11582  addsubsub23  11722  muladd  11748  nnadd1com  12361  nnaddcom  12362  nnadddir  12394  add1p1  12597  div4p1lem1div2  12601  zpnn0elfzo1  13874  flhalf  13970  fldiv  14000  binom3  14368  bernneq  14373  discr1  14383  ccatass  14734  cshweqrep  14972  01sqrexlem7  15415  sqreulem  15527  isercoll2  15836  caucvgrlem  15840  iseraltlem2  15850  bcxmas  16004  bpoly4  16225  efsep  16278  efi4p  16305  efival  16320  pwp1fsum  16561  flodddiv4  16585  sadadd2lem2  16620  sadadd2lem  16629  sadasslem  16640  pcadd2  17068  prmreclem6  17099  4sqlem11  17133  vdwapun  17152  vdwlem3  17161  vdwlem6  17164  vdwlem8  17166  vdwlem9  17167  prmgaplem8  17236  psgnunilem2  19709  sylow1lem1  19812  efgredlemc  19959  psdmul  22487  opnreen  25151  ovolunlem1a  25817  nulmbl2  25857  unmbl  25858  volinun  25867  uniioombllem5  25908  itgcnlem  26110  ditgsplit  26181  dvnadd  26249  dvntaylp  26698  ulmshft  26717  ulmcn  26726  tangtx  26834  heron  27166  quad2  27167  dcubic1lem  27171  mcubic  27175  binom4  27178  dquartlem1  27179  dquartlem2  27180  dquart  27181  quart1  27184  quart  27189  lgamcvg2  27382  basellem2  27409  basellem3  27410  basellem8  27415  ppiub  27531  bcp1ctr  27606  bposlem9  27619  2lgslem3c  27725  2lgslem3d  27726  selberg3  27886  pntpbnd2  27914  pntibndlem2  27918  pntlemg  27925  pntlemk  27933  pntlemo  27934  axeuclidlem  29540  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  finsumvtxdg2ssteplem4  30129  wwlksnextwrd  30486  wwlksnextproplem3  30500  wwlksext2clwwlk  30648  numclwlk2lem2f  30978  numclwlk2lem2f1o  30980  smcnlem  31299  stadd3i  32850  golem1  32873  quad3d  33341  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2  33694  archirngz  33750  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  subfacval2  35952  subfaclim  35953  subfacval3  35954  faclimlem1  36508  faclim2  36513  fwddifnp1  36930  dnizphlfeqhlf  37342  dnibndlem10  37353  dnibndlem13  37356  qdiff  38249  poimirlem16  38555  itg2addnclem3  38592  itg2addnc  38593  areacirclem1  38627  aks4d1p1p2  43121  posbezout  43151  2np3bcnp1  43195  sticksstones12a  43208  bcle2d  43230  aks6d1c7lem1  43231  quadfac  43256  readdridaddlidd  43309  resubeulem1  43427  resubeulem2  43428  readdsub  43436  resubsub4  43441  resubidaddlidlem  43446  sn-addlid  43456  renegneg  43464  readdcan2  43465  renegid2  43466  sn-it0e0  43468  sn-negex12  43469  sn-addcand  43472  sn-addrid  43473  sn-addcan2d  43474  sn-subeu  43479  sn-0tie0  43516  zaddcomlem  43528  zaddcom  43529  cnreeu  43555  dffltz  43671  3cubeslem2  43696  3cubeslem3l  43697  3cubeslem3r  43698  jm2.19lem3  43998  jm2.25  44006  int-addassocd  45174  binomcxplemnotnn0  45340  sub2times  46289  fperiodmullem  46319  dvnmul  46953  wallispilem4  47078  wallispi2lem2  47082  stirlinglem6  47089  dirkerper  47106  dirkertrigeqlem1  47108  dirkertrigeqlem2  47109  dirkertrigeqlem3  47110  dirkercncflem1  47113  fourierdlem26  47143  fourierdlem35  47152  fourierdlem42  47159  fourierdlem51  47167  fourierdlem64  47180  fourierdlem111  47227  hoidmv1lelem2  47602  hoidmvlelem2  47606  smflimlem4  47784  deccarry  48381  sqrtpwpw2p  48623  fmtnorec2lem  48627  fmtnorec3  48633  fmtnorec4  48634  mod42tp1mod8  48687  gpg5nbgrvtx13starlem2  49170  itcovalpclem2  49783  ackval1  49793  ackval2  49794  itscnhlc0yqe  49871  itsclquadb  49888  sinhpcosh  50833  crosspdotsumlem  50964  crossp3d  50967  veroquadgsumlem  50983