Theorem npcand 9977

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

Hypotheses

Ref	Expression
negidd.1	|- ( ph -> A e. CC )
pncand.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
npcand	|- ( ph -> ( ( A - B ) + B ) = A )

Proof of Theorem npcand

Step	Hyp	Ref	Expression
1		negidd.1	. 2 |- ( ph -> A e. CC )
2		pncand.2	. 2 |- ( ph -> B e. CC )
3		npcan 9871	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
4	1, 2, 3	syl2anc 671	1 |- ( ph -> ( ( A - B ) + B ) = A )

Syntax hints:   -> wi 4   = wceq 1448   e. wcel 1891  (class class class)co 6276   CCcc 9524   + caddc 9529   - cmin 9847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-po 4733  df-so 4734  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-ltxr 9667  df-sub 9849

This theorem is referenced by:  addlsub  10025  npcan1  10033  ltsubadd  10073  lesubadd  10075  lesub1  10097  lincmb01cmp  11766  expaddzlem  12309  bcpasc  12500  bcn2m1  12503  swrdccatwrd  12823  cshwidxmod  12904  shftuz  13143  o1dif  13704  arisum2  13930  ntrivcvg  13964  ntrivcvgtail  13967  prodrblem  13994  fprodser  14014  fprodm1  14032  risefacval2  14074  fallfacval2  14075  fallfacfwd  14100  binomfallfaclem2  14104  sin01bnd  14250  moddvds  14323  dvdsexp  14372  bitscmp  14423  hashdvds  14734  vdwlem5  14946  vdwlem6  14947  vdwlem8  14949  srgbinomlem4  17787  uniioombllem3  22555  i1faddlem  22663  itg1addlem4  22669  dvcnp2  22886  ftc1lem4  23003  dgrcolem2  23240  plydivlem4  23261  aaliou3lem8  23313  dvtaylp  23337  dvntaylp0  23339  taylthlem1  23340  efif1olem4  23506  tanarg  23580  quart1  23794  dmgmaddnn0  23964  lgamgulm2  23973  gamfac  24004  basellem9  24027  chtublem  24151  logexprlim  24165  dchrptlem1  24204  lgsquadlem1  24294  mudivsum  24380  logsqvma  24392  log2sumbnd  24394  selberglem2  24396  pntrlog2bndlem5  24431  pntlem3  24459  ostth2lem2  24484  brbtwn2  24947  cusgrasize2inds  25217  fargshiftfo  25378  clwlkisclwwlklem1  25527  clwwlkel  25533  clwwlkf  25534  clwwisshclww  25547  numclwlk1lem2fo  25835  numclwwlk2  25847  fzspl  28376  fzsplit3  28378  bcm1n  28379  omndmul3  28483  psgnfzto1stlem  28620  ballotlemfc0  29331  ballotlemfcc  29332  signstfvn  29464  bcm1nt  30379  itg2addnclem  31995  ftc1cnnclem  32017  ftc1anc  32027  caushft  32092  pellexlem6  35680  rmspecfund  35759  rmyluc  35787  jm2.18  35845  jm2.25  35856  hbtlem4  35987  bccm1k  36692  binomcxplemwb  36698  binomcxplemnotnn0  36706  oddfl  37518  zltlesub  37526  fzisoeu  37549  fperiodmul  37553  fzdifsuc2  37561  iccshift  37660  iooshift  37664  fmul01lt1lem2  37705  limcperiod  37750  sumnnodd  37752  cncfperiod  37798  fperdvper  37832  dvbdfbdioolem2  37843  dvnmul  37860  itgsinexp  37873  itgperiod  37900  stoweidlem11  37928  stoweidlem14  37931  stoweidlem26  37943  stoweidlem34  37952  wallispilem5  37988  stirlinglem5  37997  stirlinglem11  38003  stirlinglem12  38004  dirkercncflem1  38022  fourierdlem11  38037  fourierdlem15  38041  fourierdlem26  38052  fourierdlem41  38068  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem48  38075  fourierdlem49  38076  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem74  38101  fourierdlem75  38102  fourierdlem79  38106  fourierdlem81  38108  fourierdlem84  38111  fourierdlem88  38115  fourierdlem90  38117  fourierdlem92  38119  fourierdlem95  38122  fourierdlem97  38124  fourierdlem103  38130  fourierdlem104  38131  fourierdlem109  38136  fourierdlem111  38138  fourierswlem  38151  fouriersw  38152  elaa2lem  38154  elaa2lemOLD  38155  etransclem23  38179  etransclem24  38180  etransclem28  38184  etransclem38  38194  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  bgoldbtbndlem4  38994  bgoldbtbnd  38995  ccatpfx  39043  cusgrsize2inds  39616  m1modmmod  40649  dignn0flhalflem1  40751