Theorem addassd 11265

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135   + caddc 11140

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

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

This theorem is referenced by:  addrid  11423  cnegex  11424  addlid  11426  addcan  11427  addcan2  11428  addcom  11429  addcomd  11445  muladd11r  11456  negeu  11480  addsubass  11500  nppcan3  11515  muladd  11677  add1p1  12500  div4p1lem1div2  12504  zpnn0elfzo1  13760  flhalf  13852  fldiv  13882  binom3  14245  bernneq  14250  discr1  14260  ccatass  14608  cshweqrep  14841  01sqrexlem7  15269  sqreulem  15380  isercoll2  15687  caucvgrlem  15691  iseraltlem2  15701  bcxmas  15853  bpoly4  16077  efsep  16128  efi4p  16155  efival  16170  pwp1fsum  16410  flodddiv4  16434  sadadd2lem2  16469  sadadd2lem  16478  sadasslem  16489  pcadd2  16910  prmreclem6  16941  4sqlem11  16975  vdwapun  16994  vdwlem3  17003  vdwlem6  17006  vdwlem8  17008  vdwlem9  17009  prmgaplem8  17078  psgnunilem2  19481  sylow1lem1  19584  efgredlemc  19731  psdmul  22118  opnreen  24789  ovolunlem1a  25467  nulmbl2  25507  unmbl  25508  volinun  25517  uniioombllem5  25558  itgcnlem  25761  ditgsplit  25832  dvnadd  25901  dvntaylp  26349  ulmshft  26369  ulmcn  26378  tangtx  26483  heron  26817  quad2  26818  dcubic1lem  26822  mcubic  26826  binom4  26829  dquartlem1  26830  dquartlem2  26831  dquart  26832  quart1  26835  quart  26840  lgamcvg2  27034  basellem2  27061  basellem3  27062  basellem8  27067  ppiub  27184  bcp1ctr  27259  bposlem9  27272  2lgslem3c  27378  2lgslem3d  27379  selberg3  27539  pntpbnd2  27567  pntibndlem2  27571  pntlemg  27578  pntlemk  27586  pntlemo  27587  axeuclidlem  28907  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  finsumvtxdg2ssteplem4  29494  wwlksnextwrd  29845  wwlksnextproplem3  29859  wwlksext2clwwlk  30004  numclwlk2lem2f  30324  numclwlk2lem2f1o  30326  smcnlem  30644  stadd3i  32195  golem1  32218  quad3d  32690  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2  33092  archirngz  33135  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  subfacval2  35151  subfaclim  35152  subfacval3  35153  faclimlem1  35702  faclim2  35707  fwddifnp1  36125  dnizphlfeqhlf  36436  dnibndlem10  36447  dnibndlem13  36450  poimirlem16  37602  itg2addnclem3  37639  itg2addnc  37640  areacirclem1  37674  aks4d1p1p2  42030  posbezout  42060  2np3bcnp1  42104  sticksstones12a  42117  bcle2d  42139  aks6d1c7lem1  42140  2xp3dxp2ge1d  42201  readdridaddlidd  42257  nnadd1com  42265  nnaddcom  42266  nnadddir  42268  resubeulem1  42368  resubeulem2  42369  readdsub  42377  resubsub4  42382  resubidaddlidlem  42387  sn-addlid  42397  renegneg  42404  readdcan2  42405  renegid2  42406  sn-it0e0  42408  sn-negex12  42409  sn-addcand  42412  sn-addrid  42413  sn-addcan2d  42414  sn-subeu  42419  sn-0tie0  42432  zaddcomlem  42444  zaddcom  42445  cnreeu  42463  dffltz  42607  3cubeslem2  42659  3cubeslem3l  42660  3cubeslem3r  42661  jm2.19lem3  42966  jm2.25  42974  int-addassocd  44149  binomcxplemnotnn0  44332  sub2times  45241  fperiodmullem  45272  dvnmul  45915  wallispilem4  46040  wallispi2lem2  46044  stirlinglem6  46051  dirkerper  46068  dirkertrigeqlem1  46070  dirkertrigeqlem2  46071  dirkertrigeqlem3  46072  dirkercncflem1  46075  fourierdlem26  46105  fourierdlem35  46114  fourierdlem42  46121  fourierdlem51  46129  fourierdlem64  46142  fourierdlem111  46189  hoidmv1lelem2  46564  hoidmvlelem2  46568  smflimlem4  46746  deccarry  47281  sqrtpwpw2p  47483  fmtnorec2lem  47487  fmtnorec3  47493  fmtnorec4  47494  mod42tp1mod8  47547  gpg5nbgrvtx13starlem2  47986  itcovalpclem2  48550  ackval1  48560  ackval2  48561  itscnhlc0yqe  48638  itsclquadb  48655  sinhpcosh  49267