MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  npcand Unicode version

Theorem npcand 9340
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
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 pncand.2 . 2  |-  ( ph  ->  B  e.  CC )
3 npcan 9239 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  -  B )  +  B
)  =  A )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( ( A  -  B )  +  B
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717  (class class class)co 6013   CCcc 8914    + caddc 8919    - cmin 9216
This theorem is referenced by:  ltsubadd  9423  lesubadd  9425  lesub1  9447  lincmb01cmp  10963  expaddzlem  11343  bcpasc  11532  bcn2m1  11535  shftuz  11804  o1dif  12343  arisum2  12560  sin01bnd  12706  moddvds  12779  dvdsexp  12825  bitscmp  12870  hashdvds  13084  vdwlem5  13273  vdwlem6  13274  vdwlem8  13276  uniioombllem3  19337  i1faddlem  19445  itg1addlem4  19451  dvcnp2  19666  ftc1lem4  19783  dgrcolem2  20052  plydivlem4  20073  aaliou3lem8  20122  dvtaylp  20146  dvntaylp0  20148  taylthlem1  20149  efif1olem4  20307  tanarg  20374  quart1  20556  basellem9  20731  chtublem  20855  logexprlim  20869  dchrptlem1  20908  lgsquadlem1  20998  mudivsum  21084  logsqvma  21096  log2sumbnd  21098  selberglem2  21100  pntrlog2bndlem5  21135  pntlem3  21163  ostth2lem2  21188  cusgrasize2inds  21345  fargshiftfo  21466  fzspl  23978  fzsplit3  23979  bcm1n  23980  ballotlemfc0  24522  ballotlemfcc  24523  dmgmaddnn0  24583  lgamgulm2  24592  gamfac  24623  ntrivcvg  24997  ntrivcvgtail  25000  prodrblem  25027  fprodser  25047  fprodm1  25062  fprodshft  25072  risefacval2  25088  fallfacval2  25089  fallfacfwd  25112  brbtwn2  25551  itg2addnclem  25950  itg2addnc  25952  ftc1cnnclem  25971  caushft  26151  pellexlem6  26581  rmspecfund  26656  rmyluc  26684  jm2.18  26743  jm2.25  26754  hbtlem4  26992  fmul01lt1lem2  27376  itgsinexp  27410  stoweidlem11  27421  stoweidlem14  27424  stoweidlem26  27436  stoweidlem34  27444  wallispilem5  27479  stirlinglem5  27488  stirlinglem11  27494  stirlinglem12  27495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-mulcom 8980  ax-addass 8981  ax-mulass 8982  ax-distr 8983  ax-i2m1 8984  ax-1ne0 8985  ax-1rid 8986  ax-rnegex 8987  ax-rrecex 8988  ax-cnre 8989  ax-pre-lttri 8990  ax-pre-lttrn 8991  ax-pre-ltadd 8992
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-mpt 4202  df-id 4432  df-po 4437  df-so 4438  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-riota 6478  df-er 6834  df-en 7039  df-dom 7040  df-sdom 7041  df-pnf 9048  df-mnf 9049  df-ltxr 9051  df-sub 9218
  Copyright terms: Public domain W3C validator