Theorem addassd 11196

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071

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

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

This theorem is referenced by:  addrid  11354  cnegex  11355  addlid  11357  addcan  11358  addcan2  11359  addcom  11360  addcomd  11376  muladd11r  11387  negeu  11411  addsubass  11431  nppcan3  11446  addsubsub23  11586  muladd  11610  add1p1  12433  div4p1lem1div2  12437  zpnn0elfzo1  13700  flhalf  13792  fldiv  13822  binom3  14189  bernneq  14194  discr1  14204  ccatass  14553  cshweqrep  14786  01sqrexlem7  15214  sqreulem  15326  isercoll2  15635  caucvgrlem  15639  iseraltlem2  15649  bcxmas  15801  bpoly4  16025  efsep  16078  efi4p  16105  efival  16120  pwp1fsum  16361  flodddiv4  16385  sadadd2lem2  16420  sadadd2lem  16429  sadasslem  16440  pcadd2  16861  prmreclem6  16892  4sqlem11  16926  vdwapun  16945  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  prmgaplem8  17029  psgnunilem2  19425  sylow1lem1  19528  efgredlemc  19675  psdmul  22053  opnreen  24720  ovolunlem1a  25397  nulmbl2  25437  unmbl  25438  volinun  25447  uniioombllem5  25488  itgcnlem  25691  ditgsplit  25762  dvnadd  25831  dvntaylp  26279  ulmshft  26299  ulmcn  26308  tangtx  26414  heron  26748  quad2  26749  dcubic1lem  26753  mcubic  26757  binom4  26760  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1  26766  quart  26771  lgamcvg2  26965  basellem2  26992  basellem3  26993  basellem8  26998  ppiub  27115  bcp1ctr  27190  bposlem9  27203  2lgslem3c  27309  2lgslem3d  27310  selberg3  27470  pntpbnd2  27498  pntibndlem2  27502  pntlemg  27509  pntlemk  27517  pntlemo  27518  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  finsumvtxdg2ssteplem4  29476  wwlksnextwrd  29827  wwlksnextproplem3  29841  wwlksext2clwwlk  29986  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  smcnlem  30626  stadd3i  32177  golem1  32200  quad3d  32673  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  archirngz  33143  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  subfacval2  35174  subfaclim  35175  subfacval3  35176  faclimlem1  35730  faclim2  35735  fwddifnp1  36153  dnizphlfeqhlf  36464  dnibndlem10  36475  dnibndlem13  36478  poimirlem16  37630  itg2addnclem3  37667  itg2addnc  37668  areacirclem1  37702  aks4d1p1p2  42058  posbezout  42088  2np3bcnp1  42132  sticksstones12a  42145  bcle2d  42167  aks6d1c7lem1  42168  readdridaddlidd  42246  nnadd1com  42255  nnaddcom  42256  nnadddir  42258  resubeulem1  42363  resubeulem2  42364  readdsub  42372  resubsub4  42377  resubidaddlidlem  42382  sn-addlid  42392  renegneg  42400  readdcan2  42401  renegid2  42402  sn-it0e0  42404  sn-negex12  42405  sn-addcand  42408  sn-addrid  42409  sn-addcan2d  42410  sn-subeu  42415  sn-0tie0  42439  zaddcomlem  42451  zaddcom  42452  cnreeu  42478  dffltz  42622  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  jm2.19lem3  42980  jm2.25  42988  int-addassocd  44163  binomcxplemnotnn0  44345  sub2times  45271  fperiodmullem  45301  dvnmul  45941  wallispilem4  46066  wallispi2lem2  46070  stirlinglem6  46077  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem1  46101  fourierdlem26  46131  fourierdlem35  46140  fourierdlem42  46147  fourierdlem51  46155  fourierdlem64  46168  fourierdlem111  46215  hoidmv1lelem2  46590  hoidmvlelem2  46594  smflimlem4  46772  deccarry  47312  sqrtpwpw2p  47539  fmtnorec2lem  47543  fmtnorec3  47549  fmtnorec4  47550  mod42tp1mod8  47603  gpg5nbgrvtx13starlem2  48063  itcovalpclem2  48660  ackval1  48670  ackval2  48671  itscnhlc0yqe  48748  itsclquadb  48765  sinhpcosh  49729