Theorem subsubd 11560

Description: Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
subaddd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
subsubd	⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))

Proof of Theorem subsubd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subaddd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		subsub 11451	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))
5	1, 2, 3, 4	syl3anc 1386	1 ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  (class class class)co 7385  ℂcc 11061   + caddc 11066   − cmin 11404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-ltxr 11211  df-sub 11406

This theorem is referenced by:  addsubsub23  11585  subaddmulsub  11640  uzsubsubfz  13541  bcm1k  14318  swrds2m  14944  crre  15117  imval2  15154  cvgcmp  15820  arisum2  15867  mertenslem1  15890  binomfallfaclem2  16046  fallfacval4  16049  bpolydiflem  16060  bpoly3  16064  bpoly4  16065  cos01bnd  16194  prmdiv  16796  vfermltlALT  16814  dvle  26042  dvfsumlem2  26062  efif1olem2  26578  affineequiv  26858  heron  26873  dquart  26888  quartlem1  26892  acosneg  26922  efiatan2  26952  atans2  26966  birthdaylem2  26987  lgamcvg2  27089  wilthlem2  27103  basellem5  27119  gausslemma2dlem1a  27399  pntrlog2bndlem4  27614  pntrlog2bndlem5  27615  pntrlog2bndlem6  27617  colinearalglem2  29047  axsegconlem9  29065  clwlkclwwlklem2a1  30133  clwlkclwwlklem2a4  30138  clwwlkext2edg  30197  numclwwlk1lem2foalem  30492  numclwwlk1lem2fo  30499  wrdt2ind  33085  constrrtcc  33986  subfacp1lem5  35482  poimirlem29  38096  itg2addnclem  38118  itg2addnclem3  38120  bcle2d  42744  rmspecsqrtnq  43431  sub31  45817  infleinflem2  45894  stoweidlem26  46548  fourierdlem19  46648  fourierdlem63  46691  fourierdlem107  46735  ovolval5lem1  47174  sin5tlem5  47419  fmtnorec4  48106  itcovalt2lem2lem2  49244