Theorem addassd 11090

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  (class class class)co 7329  ℂcc 10962   + caddc 10967

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  addid1  11248  cnegex  11249  addid2  11251  addcan  11252  addcan2  11253  addcom  11254  addcomd  11270  muladd11r  11281  negeu  11304  addsubass  11324  nppcan3  11338  muladd  11500  add1p1  12317  div4p1lem1div2  12321  zpnn0elfzo1  13554  flhalf  13643  fldiv  13673  binom3  14032  bernneq  14037  discr1  14047  ccatass  14384  cshweqrep  14624  sqrlem7  15051  sqreulem  15162  isercoll2  15471  caucvgrlem  15475  iseraltlem2  15485  bcxmas  15638  bpoly4  15860  efsep  15910  efi4p  15937  efival  15952  pwp1fsum  16191  flodddiv4  16213  sadadd2lem2  16248  sadadd2lem  16257  sadasslem  16268  pcadd2  16680  prmreclem6  16711  4sqlem11  16745  vdwapun  16764  vdwlem3  16773  vdwlem6  16776  vdwlem8  16778  vdwlem9  16779  prmgaplem8  16848  psgnunilem2  19191  sylow1lem1  19291  efgredlemc  19438  opnreen  24092  ovolunlem1a  24758  nulmbl2  24798  unmbl  24799  volinun  24808  uniioombllem5  24849  itgcnlem  25052  ditgsplit  25123  dvnadd  25191  dvntaylp  25628  ulmshft  25647  ulmcn  25656  tangtx  25760  heron  26086  quad2  26087  dcubic1lem  26091  mcubic  26095  binom4  26098  dquartlem1  26099  dquartlem2  26100  dquart  26101  quart1  26104  quart  26109  lgamcvg2  26302  basellem2  26329  basellem3  26330  basellem8  26335  ppiub  26450  bcp1ctr  26525  bposlem9  26538  2lgslem3c  26644  2lgslem3d  26645  selberg3  26805  pntpbnd2  26833  pntibndlem2  26837  pntlemg  26844  pntlemk  26852  pntlemo  26853  axeuclidlem  27532  axcontlem2  27535  axcontlem4  27537  axcontlem7  27540  finsumvtxdg2ssteplem4  28117  wwlksnextwrd  28463  wwlksnextproplem3  28477  wwlksext2clwwlk  28622  numclwlk2lem2f  28942  numclwlk2lem2f1o  28944  smcnlem  29260  stadd3i  30811  golem1  30834  cycpmco2lem3  31595  cycpmco2lem4  31596  cycpmco2lem5  31597  cycpmco2lem6  31598  cycpmco2  31600  archirngz  31643  subfacval2  33361  subfaclim  33362  subfacval3  33363  faclimlem1  33915  faclim2  33920  fwddifnp1  34558  dnizphlfeqhlf  34747  dnibndlem10  34758  dnibndlem13  34761  poimirlem16  35891  itg2addnclem3  35928  itg2addnc  35929  areacirclem1  35963  aks4d1p1p2  40325  2np3bcnp1  40350  sticksstones12a  40363  2xp3dxp2ge1d  40412  readdid1addid2d  40544  nnadd1com  40547  nnaddcom  40548  nnadddir  40550  resubeulem1  40608  resubeulem2  40609  readdsub  40617  resubsub4  40622  resubidaddid1lem  40627  sn-addid2  40637  renegneg  40644  readdcan2  40645  renegid2  40646  sn-it0e0  40647  sn-negex12  40648  sn-addcand  40651  sn-addid1  40652  sn-addcan2d  40653  sn-subeu  40658  sn-0tie0  40671  cnreeu  40688  dffltz  40721  3cubeslem2  40757  3cubeslem3l  40758  3cubeslem3r  40759  jm2.19lem3  41064  jm2.25  41072  int-addassocd  42095  binomcxplemnotnn0  42284  sub2times  43137  fperiodmullem  43166  dvnmul  43809  wallispilem4  43934  wallispi2lem2  43938  stirlinglem6  43945  dirkerper  43962  dirkertrigeqlem1  43964  dirkertrigeqlem2  43965  dirkertrigeqlem3  43966  dirkercncflem1  43969  fourierdlem26  43999  fourierdlem35  44008  fourierdlem42  44015  fourierdlem51  44023  fourierdlem64  44036  fourierdlem111  44083  hoidmv1lelem2  44456  hoidmvlelem2  44460  smflimlem4  44638  deccarry  45143  sqrtpwpw2p  45330  fmtnorec2lem  45334  fmtnorec3  45340  fmtnorec4  45341  mod42tp1mod8  45394  itcovalpclem2  46357  ackval1  46367  ackval2  46368  itscnhlc0yqe  46445  itsclquadb  46462  sinhpcosh  46782