Theorem addassd 11358

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   + caddc 11230

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11292

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11517  cnegex  11518  addlid  11520  addcan  11521  addcan2  11522  addcom  11523  addcomd  11539  muladd11r  11550  negeu  11574  addsubass  11594  nppcan3  11609  addsubsub23  11749  muladd  11775  nnadd1com  12388  nnaddcom  12389  nnadddir  12421  add1p1  12624  div4p1lem1div2  12628  zpnn0elfzo1  13901  flhalf  13997  fldiv  14027  binom3  14395  bernneq  14400  discr1  14410  ccatass  14761  cshweqrep  15000  01sqrexlem7  15444  sqreulem  15556  isercoll2  15865  caucvgrlem  15869  iseraltlem2  15879  bcxmas  16033  bpoly4  16254  efsep  16307  efi4p  16334  efival  16349  pwp1fsum  16590  flodddiv4  16614  sadadd2lem2  16649  sadadd2lem  16658  sadasslem  16669  pcadd2  17097  prmreclem6  17128  4sqlem11  17162  vdwapun  17181  vdwlem3  17190  vdwlem6  17193  vdwlem8  17195  vdwlem9  17196  prmgaplem8  17265  psgnunilem2  19739  sylow1lem1  19842  efgredlemc  19989  psdmul  22517  opnreen  25181  ovolunlem1a  25847  nulmbl2  25887  unmbl  25888  volinun  25897  uniioombllem5  25938  itgcnlem  26140  ditgsplit  26211  dvnadd  26279  dvntaylp  26728  ulmshft  26747  ulmcn  26756  tangtx  26864  heron  27196  quad2  27197  dcubic1lem  27201  mcubic  27205  binom4  27208  dquartlem1  27209  dquartlem2  27210  dquart  27211  quart1  27214  quart  27219  lgamcvg2  27412  basellem2  27439  basellem3  27440  basellem8  27445  ppiub  27561  bcp1ctr  27636  bposlem9  27649  2lgslem3c  27755  2lgslem3d  27756  selberg3  27916  pntpbnd2  27944  pntibndlem2  27948  pntlemg  27955  pntlemk  27963  pntlemo  27964  axeuclidlem  29570  axcontlem2  29573  axcontlem4  29575  axcontlem7  29578  finsumvtxdg2ssteplem4  30159  wwlksnextwrd  30516  wwlksnextproplem3  30530  wwlksext2clwwlk  30678  numclwlk2lem2f  31008  numclwlk2lem2f1o  31010  smcnlem  31329  stadd3i  32880  golem1  32903  quad3d  33411  cycpmco2lem3  33759  cycpmco2lem4  33760  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2  33764  archirngz  33820  constrrtlc1  34434  constrrtcclem  34436  constrrtcc  34437  cos9thpiminplylem1  34484  cos9thpiminplylem2  34485  subfacval2  36119  subfaclim  36120  subfacval3  36121  faclimlem1  36686  faclim2  36691  fwddifnp1  37108  dnizphlfeqhlf  37520  dnibndlem10  37531  dnibndlem13  37534  qdiff  38440  poimirlem16  38746  itg2addnclem3  38783  itg2addnc  38784  areacirclem1  38818  aks4d1p1p2  43312  posbezout  43342  2np3bcnp1  43386  sticksstones12a  43399  bcle2d  43421  aks6d1c7lem1  43422  quadfac  43447  readdridaddlidd  43501  resubeulem1  43619  resubeulem2  43620  readdsub  43628  resubsub4  43633  resubidaddlidlem  43638  sn-addlid  43648  renegneg  43656  readdcan2  43657  renegid2  43658  sn-it0e0  43660  sn-negex12  43661  sn-addcand  43664  sn-addrid  43665  sn-addcan2d  43666  sn-subeu  43671  sn-0tie0  43708  zaddcomlem  43720  zaddcom  43721  cnreeu  43747  dffltz  43863  3cubeslem2  43888  3cubeslem3l  43889  3cubeslem3r  43890  jm2.19lem3  44191  jm2.25  44199  int-addassocd  45366  binomcxplemnotnn0  45532  sub2times  46494  fperiodmullem  46524  dvnmul  47158  wallispilem4  47283  wallispi2lem2  47287  stirlinglem6  47294  dirkerper  47311  dirkertrigeqlem1  47313  dirkertrigeqlem2  47314  dirkertrigeqlem3  47315  dirkercncflem1  47318  fourierdlem26  47348  fourierdlem35  47357  fourierdlem42  47364  fourierdlem51  47372  fourierdlem64  47385  fourierdlem111  47432  hoidmv1lelem2  47807  hoidmvlelem2  47811  smflimlem4  47989  deccarry  48586  sqrtpwpw2p  48828  fmtnorec2lem  48832  fmtnorec3  48838  fmtnorec4  48839  mod42tp1mod8  48892  gpg5nbgrvtx13starlem2  49375  itcovalpclem2  49988  ackval1  49998  ackval2  49999  itscnhlc0yqe  50076  itsclquadb  50093  sinhpcosh  51113  crosspdotsumlem  51244  crossp3d  51247  veroquadgsumlem  51263