Theorem addassd 11167

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

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

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

This theorem is referenced by:  addrid  11326  cnegex  11327  addlid  11329  addcan  11330  addcan2  11331  addcom  11332  addcomd  11348  muladd11r  11359  negeu  11383  addsubass  11403  nppcan3  11418  addsubsub23  11558  muladd  11582  nnadd1com  12200  nnaddcom  12201  nnadddir  12233  add1p1  12428  div4p1lem1div2  12432  zpnn0elfzo1  13694  flhalf  13789  fldiv  13819  binom3  14186  bernneq  14191  discr1  14201  ccatass  14551  cshweqrep  14783  01sqrexlem7  15210  sqreulem  15322  isercoll2  15631  caucvgrlem  15635  iseraltlem2  15645  bcxmas  15800  bpoly4  16024  efsep  16077  efi4p  16104  efival  16119  pwp1fsum  16360  flodddiv4  16384  sadadd2lem2  16419  sadadd2lem  16428  sadasslem  16439  pcadd2  16861  prmreclem6  16892  4sqlem11  16926  vdwapun  16945  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  prmgaplem8  17029  psgnunilem2  19470  sylow1lem1  19573  efgredlemc  19720  psdmul  22132  opnreen  24797  ovolunlem1a  25463  nulmbl2  25503  unmbl  25504  volinun  25513  uniioombllem5  25554  itgcnlem  25757  ditgsplit  25828  dvnadd  25896  dvntaylp  26336  ulmshft  26355  ulmcn  26364  tangtx  26469  heron  26802  quad2  26803  dcubic1lem  26807  mcubic  26811  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1  26820  quart  26825  lgamcvg2  27018  basellem2  27045  basellem3  27046  basellem8  27051  ppiub  27167  bcp1ctr  27242  bposlem9  27255  2lgslem3c  27361  2lgslem3d  27362  selberg3  27522  pntpbnd2  27550  pntibndlem2  27554  pntlemg  27561  pntlemk  27569  pntlemo  27570  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  finsumvtxdg2ssteplem4  29617  wwlksnextwrd  29965  wwlksnextproplem3  29979  wwlksext2clwwlk  30127  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  smcnlem  30768  stadd3i  32319  golem1  32342  quad3d  32822  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  archirngz  33250  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  subfacval2  35369  subfaclim  35370  subfacval3  35371  faclimlem1  35925  faclim2  35930  fwddifnp1  36347  dnizphlfeqhlf  36736  dnibndlem10  36747  dnibndlem13  36750  qdiff  37641  poimirlem16  37957  itg2addnclem3  37994  itg2addnc  37995  areacirclem1  38029  aks4d1p1p2  42509  posbezout  42539  2np3bcnp1  42583  sticksstones12a  42596  bcle2d  42618  aks6d1c7lem1  42619  readdridaddlidd  42696  resubeulem1  42807  resubeulem2  42808  readdsub  42816  resubsub4  42821  resubidaddlidlem  42826  sn-addlid  42836  renegneg  42844  readdcan2  42845  renegid2  42846  sn-it0e0  42848  sn-negex12  42849  sn-addcand  42852  sn-addrid  42853  sn-addcan2d  42854  sn-subeu  42859  sn-0tie0  42896  zaddcomlem  42908  zaddcom  42909  cnreeu  42935  dffltz  43067  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  jm2.19lem3  43419  jm2.25  43427  int-addassocd  44601  binomcxplemnotnn0  44783  sub2times  45706  fperiodmullem  45736  dvnmul  46371  wallispilem4  46496  wallispi2lem2  46500  stirlinglem6  46507  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem1  46531  fourierdlem26  46561  fourierdlem35  46570  fourierdlem42  46577  fourierdlem51  46585  fourierdlem64  46598  fourierdlem111  46645  hoidmv1lelem2  47020  hoidmvlelem2  47024  smflimlem4  47202  deccarry  47759  sqrtpwpw2p  48001  fmtnorec2lem  48005  fmtnorec3  48011  fmtnorec4  48012  mod42tp1mod8  48065  gpg5nbgrvtx13starlem2  48548  itcovalpclem2  49147  ackval1  49157  ackval2  49158  itscnhlc0yqe  49235  itsclquadb  49252  sinhpcosh  50215