Theorem addassd 11203

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078

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

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

This theorem is referenced by:  addrid  11361  cnegex  11362  addlid  11364  addcan  11365  addcan2  11366  addcom  11367  addcomd  11383  muladd11r  11394  negeu  11418  addsubass  11438  nppcan3  11453  addsubsub23  11593  muladd  11617  add1p1  12440  div4p1lem1div2  12444  zpnn0elfzo1  13707  flhalf  13799  fldiv  13829  binom3  14196  bernneq  14201  discr1  14211  ccatass  14560  cshweqrep  14793  01sqrexlem7  15221  sqreulem  15333  isercoll2  15642  caucvgrlem  15646  iseraltlem2  15656  bcxmas  15808  bpoly4  16032  efsep  16085  efi4p  16112  efival  16127  pwp1fsum  16368  flodddiv4  16392  sadadd2lem2  16427  sadadd2lem  16436  sadasslem  16447  pcadd2  16868  prmreclem6  16899  4sqlem11  16933  vdwapun  16952  vdwlem3  16961  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  prmgaplem8  17036  psgnunilem2  19432  sylow1lem1  19535  efgredlemc  19682  psdmul  22060  opnreen  24727  ovolunlem1a  25404  nulmbl2  25444  unmbl  25445  volinun  25454  uniioombllem5  25495  itgcnlem  25698  ditgsplit  25769  dvnadd  25838  dvntaylp  26286  ulmshft  26306  ulmcn  26315  tangtx  26421  heron  26755  quad2  26756  dcubic1lem  26760  mcubic  26764  binom4  26767  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1  26773  quart  26778  lgamcvg2  26972  basellem2  26999  basellem3  27000  basellem8  27005  ppiub  27122  bcp1ctr  27197  bposlem9  27210  2lgslem3c  27316  2lgslem3d  27317  selberg3  27477  pntpbnd2  27505  pntibndlem2  27509  pntlemg  27516  pntlemk  27524  pntlemo  27525  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  finsumvtxdg2ssteplem4  29483  wwlksnextwrd  29834  wwlksnextproplem3  29848  wwlksext2clwwlk  29993  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  smcnlem  30633  stadd3i  32184  golem1  32207  quad3d  32680  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  archirngz  33150  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  subfacval2  35181  subfaclim  35182  subfacval3  35183  faclimlem1  35737  faclim2  35742  fwddifnp1  36160  dnizphlfeqhlf  36471  dnibndlem10  36482  dnibndlem13  36485  poimirlem16  37637  itg2addnclem3  37674  itg2addnc  37675  areacirclem1  37709  aks4d1p1p2  42065  posbezout  42095  2np3bcnp1  42139  sticksstones12a  42152  bcle2d  42174  aks6d1c7lem1  42175  readdridaddlidd  42253  nnadd1com  42262  nnaddcom  42263  nnadddir  42265  resubeulem1  42370  resubeulem2  42371  readdsub  42379  resubsub4  42384  resubidaddlidlem  42389  sn-addlid  42399  renegneg  42407  readdcan2  42408  renegid2  42409  sn-it0e0  42411  sn-negex12  42412  sn-addcand  42415  sn-addrid  42416  sn-addcan2d  42417  sn-subeu  42422  sn-0tie0  42446  zaddcomlem  42458  zaddcom  42459  cnreeu  42485  dffltz  42629  3cubeslem2  42680  3cubeslem3l  42681  3cubeslem3r  42682  jm2.19lem3  42987  jm2.25  42995  int-addassocd  44170  binomcxplemnotnn0  44352  sub2times  45278  fperiodmullem  45308  dvnmul  45948  wallispilem4  46073  wallispi2lem2  46077  stirlinglem6  46084  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem1  46108  fourierdlem26  46138  fourierdlem35  46147  fourierdlem42  46154  fourierdlem51  46162  fourierdlem64  46175  fourierdlem111  46222  hoidmv1lelem2  46597  hoidmvlelem2  46601  smflimlem4  46779  deccarry  47316  sqrtpwpw2p  47543  fmtnorec2lem  47547  fmtnorec3  47553  fmtnorec4  47554  mod42tp1mod8  47607  gpg5nbgrvtx13starlem2  48067  itcovalpclem2  48664  ackval1  48674  ackval2  48675  itscnhlc0yqe  48752  itsclquadb  48769  sinhpcosh  49733