Theorem subsub4d 11640

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

Hypotheses

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

Assertion

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

Proof of Theorem subsub4d

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144   + caddc 11149   − cmin 11482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291  df-sub 11484

This theorem is referenced by:  subaddmulsub  11715  sub1m1  12502  cnm2m1cnm3  12503  nn0n0n1ge2  12577  ubmelm1fzo  13768  hashf1  14458  ccatass  14578  isercolllem1  15651  caucvgrlem  15659  fsumparts  15792  incexclem  15822  arisum2  15847  pwdif  15854  bpolydiflem  16038  bpoly4  16043  sin01bnd  16169  cos01bnd  16170  vdwlem5  16961  vdwlem8  16964  efgredleme  19705  opnreen  24767  pjthlem1  25385  dveflem  25931  dvcvx  25973  dvfsumlem1  25980  efif1olem2  26497  tanarg  26573  dcubic1  26797  dquartlem1  26803  tanatan  26871  atans2  26883  harmonicbnd4  26963  basellem5  27037  logfaclbnd  27175  bcmono  27230  lgsquadlem1  27333  mulogsumlem  27484  mulog2sumlem1  27487  vmalogdivsum  27492  selbergr  27521  selberg3r  27522  brbtwn2  28736  colinearalglem1  28737  colinearalglem2  28738  colinearalglem4  28740  ax5seglem1  28759  clwlkclwwlklem2a4  29827  clwlkclwwlklem2a  29828  clwwlkext2edg  29886  clwwlknonex2lem1  29937  clwwlknonex2lem2  29938  pjhthlem1  31221  lt2addrd  32542  cycpmco2lem6  32873  ballotlemfp1  34144  signstfveq0  34242  revpfxsfxrev  34758  revwlk  34767  bcprod  35365  dnibndlem10  35995  lcmineqlem10  41541  sticksstones10  41659  sticksstones12a  41661  bcle2d  41683  suplesup  44750  fperdvper  45336  dvnxpaek  45359  itgsinexp  45372  stoweidlem26  45443  stoweidlem34  45451  stirlinglem5  45495  fourierdlem26  45550  fourierdlem107  45630  vonioolem1  46097  dignn0flhalflem1  47766  itsclc0yqsollem1  47913  2itscplem3  47931