Theorem npcand 9933

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 9828	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + B ) = A )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( ( A - B ) + B ) = A )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767  (class class class)co 6283   CCcc 9489   + caddc 9494   - cmin 9804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-resscn 9548  ax-1cn 9549  ax-icn 9550  ax-addcl 9551  ax-addrcl 9552  ax-mulcl 9553  ax-mulrcl 9554  ax-mulcom 9555  ax-addass 9556  ax-mulass 9557  ax-distr 9558  ax-i2m1 9559  ax-1ne0 9560  ax-1rid 9561  ax-rnegex 9562  ax-rrecex 9563  ax-cnre 9564  ax-pre-lttri 9565  ax-pre-lttrn 9566  ax-pre-ltadd 9567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-riota 6244  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9629  df-mnf 9630  df-ltxr 9632  df-sub 9806

This theorem is referenced by:  npcan1  9983  ltsubadd  10021  lesubadd  10023  lesub1  10045  lincmb01cmp  11662  expaddzlem  12176  bcpasc  12366  bcn2m1  12369  swrdccatwrd  12655  cshwidxmod  12736  shftuz  12864  o1dif  13414  arisum2  13634  sin01bnd  13780  moddvds  13853  dvdsexp  13900  bitscmp  13946  hashdvds  14163  vdwlem5  14361  vdwlem6  14362  vdwlem8  14364  srgbinomlem4  16991  uniioombllem3  21745  i1faddlem  21851  itg1addlem4  21857  dvcnp2  22074  ftc1lem4  22191  dgrcolem2  22421  plydivlem4  22442  aaliou3lem8  22491  dvtaylp  22515  dvntaylp0  22517  taylthlem1  22518  efif1olem4  22681  tanarg  22748  quart1  22931  basellem9  23106  chtublem  23230  logexprlim  23244  dchrptlem1  23283  lgsquadlem1  23373  mudivsum  23459  logsqvma  23471  log2sumbnd  23473  selberglem2  23475  pntrlog2bndlem5  23510  pntlem3  23538  ostth2lem2  23563  brbtwn2  23900  cusgrasize2inds  24169  fargshiftfo  24330  clwlkisclwwlklem1  24479  clwwlkel  24485  clwwlkf  24486  clwwisshclww  24499  numclwlk1lem2fo  24788  numclwwlk2  24800  fzsplit3  27283  bcm1n  27284  omndmul3  27381  ballotlemfc0  28087  ballotlemfcc  28088  signstfvn  28182  dmgmaddnn0  28225  lgamgulm2  28234  gamfac  28265  ntrivcvg  28624  ntrivcvgtail  28627  prodrblem  28654  fprodser  28674  fprodm1  28689  fprodshft  28699  risefacval2  28725  fallfacval2  28726  fallfacfwd  28751  binomfallfaclem2  28755  itg2addnclem  29659  ftc1cnnclem  29681  ftc1anc  29691  caushft  29873  pellexlem6  30390  rmspecfund  30465  rmyluc  30493  jm2.18  30550  jm2.25  30561  hbtlem4  30695  oddfl  31052  zltlesub  31061  hashssle  31090  fzisoeu  31093  fperiodmul  31097  iccshift  31138  iooshift  31142  fmul01lt1lem2  31151  limcperiod  31186  sumnnodd  31188  cncfperiod  31233  fperdvper  31264  dvbdfbdioolem2  31275  itgsinexp  31288  itgiccshift  31314  itgperiod  31315  stoweidlem11  31327  stoweidlem14  31330  stoweidlem26  31342  stoweidlem34  31350  wallispilem5  31385  stirlinglem5  31394  stirlinglem11  31400  stirlinglem12  31401  dirkercncflem1  31419  fourierdlem11  31434  fourierdlem15  31438  fourierdlem26  31449  fourierdlem41  31464  fourierdlem42  31465  fourierdlem48  31471  fourierdlem49  31472  fourierdlem63  31486  fourierdlem64  31487  fourierdlem65  31488  fourierdlem74  31497  fourierdlem75  31498  fourierdlem79  31502  fourierdlem81  31504  fourierdlem84  31507  fourierdlem88  31511  fourierdlem90  31513  fourierdlem92  31515  fourierdlem97  31520  fourierdlem103  31526  fourierdlem104  31527  fourierdlem109  31532  fourierdlem111  31534  fourierswlem  31547  fouriersw  31548  bj-lsub  33752