Theorem addassd 11219

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  addrid  11378  cnegex  11379  addlid  11381  addcan  11382  addcan2  11383  addcom  11384  addcomd  11400  muladd11r  11411  negeu  11435  addsubass  11455  nppcan3  11470  addsubsub23  11610  muladd  11634  nnadd1com  12250  nnaddcom  12251  nnadddir  12283  add1p1  12486  div4p1lem1div2  12490  zpnn0elfzo1  13759  flhalf  13854  fldiv  13884  binom3  14251  bernneq  14256  discr1  14266  ccatass  14616  cshweqrep  14848  01sqrexlem7  15289  sqreulem  15401  isercoll2  15710  caucvgrlem  15714  iseraltlem2  15724  bcxmas  15879  bpoly4  16103  efsep  16156  efi4p  16183  efival  16198  pwp1fsum  16439  flodddiv4  16463  sadadd2lem2  16498  sadadd2lem  16507  sadasslem  16518  pcadd2  16940  prmreclem6  16971  4sqlem11  17005  vdwapun  17024  vdwlem3  17033  vdwlem6  17036  vdwlem8  17038  vdwlem9  17039  prmgaplem8  17108  psgnunilem2  19556  sylow1lem1  19659  efgredlemc  19806  psdmul  22289  opnreen  24950  ovolunlem1a  25616  nulmbl2  25656  unmbl  25657  volinun  25666  uniioombllem5  25707  itgcnlem  25910  ditgsplit  25981  dvnadd  26049  dvntaylp  26492  ulmshft  26511  ulmcn  26520  tangtx  26628  heron  26961  quad2  26962  dcubic1lem  26966  mcubic  26970  binom4  26973  dquartlem1  26974  dquartlem2  26975  dquart  26976  quart1  26979  quart  26984  lgamcvg2  27177  basellem2  27204  basellem3  27205  basellem8  27210  ppiub  27326  bcp1ctr  27401  bposlem9  27414  2lgslem3c  27520  2lgslem3d  27521  selberg3  27681  pntpbnd2  27709  pntibndlem2  27713  pntlemg  27720  pntlemk  27728  pntlemo  27729  axeuclidlem  29221  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  finsumvtxdg2ssteplem4  29807  wwlksnextwrd  30155  wwlksnextproplem3  30169  wwlksext2clwwlk  30317  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  smcnlem  30958  stadd3i  32509  golem1  32532  quad3d  33006  cycpmco2lem3  33361  cycpmco2lem4  33362  cycpmco2lem5  33363  cycpmco2lem6  33364  cycpmco2  33366  archirngz  33422  constrrtlc1  34039  constrrtcclem  34041  constrrtcc  34042  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  subfacval2  35550  subfaclim  35551  subfacval3  35552  faclimlem1  36106  faclim2  36111  fwddifnp1  36528  dnizphlfeqhlf  36927  dnibndlem10  36938  dnibndlem13  36941  qdiff  37831  poimirlem16  38147  itg2addnclem3  38184  itg2addnc  38185  areacirclem1  38219  aks4d1p1p2  42699  posbezout  42729  2np3bcnp1  42773  sticksstones12a  42786  bcle2d  42808  aks6d1c7lem1  42809  readdridaddlidd  42885  resubeulem1  42996  resubeulem2  42997  readdsub  43005  resubsub4  43010  resubidaddlidlem  43015  sn-addlid  43025  renegneg  43033  readdcan2  43034  renegid2  43035  sn-it0e0  43037  sn-negex12  43038  sn-addcand  43041  sn-addrid  43042  sn-addcan2d  43043  sn-subeu  43048  sn-0tie0  43085  zaddcomlem  43097  zaddcom  43098  cnreeu  43124  dffltz  43228  3cubeslem2  43278  3cubeslem3l  43279  3cubeslem3r  43280  jm2.19lem3  43580  jm2.25  43588  int-addassocd  44762  binomcxplemnotnn0  44930  sub2times  45850  fperiodmullem  45880  dvnmul  46515  wallispilem4  46640  wallispi2lem2  46644  stirlinglem6  46651  dirkerper  46668  dirkertrigeqlem1  46670  dirkertrigeqlem2  46671  dirkertrigeqlem3  46672  dirkercncflem1  46675  fourierdlem26  46705  fourierdlem35  46714  fourierdlem42  46721  fourierdlem51  46729  fourierdlem64  46742  fourierdlem111  46789  hoidmv1lelem2  47164  hoidmvlelem2  47168  smflimlem4  47346  deccarry  47903  sqrtpwpw2p  48145  fmtnorec2lem  48149  fmtnorec3  48155  fmtnorec4  48156  mod42tp1mod8  48209  gpg5nbgrvtx13starlem2  48692  itcovalpclem2  49302  ackval1  49312  ackval2  49313  itscnhlc0yqe  49390  itsclquadb  49407  sinhpcosh  50369