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

Theorem pncand 9934
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
pncand  |-  ( ph  ->  ( ( A  +  B )  -  B
)  =  A )

Proof of Theorem pncand
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 pncand.2 . 2  |-  ( ph  ->  B  e.  CC )
3 pncan 9828 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  -  B
)  =  A )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( ( A  +  B )  -  B
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802  (class class class)co 6278   CCcc 9490    + caddc 9495    - cmin 9807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-po 4787  df-so 4788  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-er 7310  df-en 7516  df-dom 7517  df-sdom 7518  df-pnf 9630  df-mnf 9631  df-ltxr 9633  df-sub 9809
This theorem is referenced by:  pncan1  9986  icoshftf1o  11649  xov1plusxeqvd  11672  zesq  12265  brfi1indlem  12507  ccatval3  12573  wrdlenccats1lenm1  12603  fsumrev2  13573  binom1dif  13621  sadcp1  13979  smupp1  14004  hashdvds  14179  pythagtriplem4  14217  pythagtriplem6  14219  pythagtriplem7  14220  pythagtriplem12  14224  pythagtriplem14  14226  pcqdiv  14255  mulgdirlem  16037  cayhamlem1  19237  blhalf  20778  pjthlem1  21722  ovolicopnf  21805  i1faddlem  21970  itg1addlem4  21976  ftc1lem4  22310  aaliou3lem8  22610  taylthlem2  22638  ulmshft  22654  efif1olem2  22799  efif1olem4  22801  quart1lem  23055  asinsin  23092  efiatan2  23117  logdiflbnd  23193  harmonicbnd4  23209  ftalem1  23215  ftalem2  23216  bcctr  23419  pcbcctr  23420  bcp1ctr  23423  2sqblem  23521  mulog2sumlem1  23588  mulog2sumlem3  23590  pntrlog2bndlem2  23632  pntrlog2bndlem4  23634  pntrlog2bndlem5  23635  pntrlog2bndlem6  23637  colinearalglem4  24081  axpaschlem  24112  wwlknimp  24556  wwlknred  24592  wwlknredwwlkn  24595  wwlkextproplem2  24611  clwlkisclwwlklem1  24656  clwlkisclwwlklem0  24657  clwwlkf  24663  wwlkext2clwwlk  24672  rusgra0edg  24824  eupatrl  24837  numclwwlk2lem1  24971  numclwlk2lem2f  24972  pjhthlem1  26178  dya2icoseg  28118  iwrdsplit  28196  fibp1  28210  ballotlemfc0  28301  ballotlemfcc  28302  ballotlemsgt1  28319  ballotlemsel1i  28321  ballotlemsima  28324  ballotlem1ri  28343  eluzmn  28361  signstfvn  28396  lgamgulmlem2  28442  lgamcvg2  28467  relgamcl  28474  pnpncand  28985  fprodp1  29070  risefacp1  29123  fallfacp1  29124  bpolydiflem  29788  fsumcube  29794  sin2h  30017  itg2addnclem  30038  itg2addnclem3  30040  ftc1cnnclem  30060  areacirclem4  30082  ssbnd  30256  jm2.19lem4  30906  jm2.23  30910  jm3.1lem1  30931  itgpowd  31155  hashnzfzclim  31200  iccshift  31494  iooshift  31498  climinf  31520  limcperiod  31542  0ellimcdiv  31563  cncfshift  31583  cncfperiod  31588  itgiccshift  31669  itgperiod  31670  stoweidlem17  31688  wallispilem4  31739  wallispilem5  31740  stirlinglem1  31745  stirlinglem5  31749  stirlinglem6  31750  stirlinglem10  31754  dirkertrigeqlem2  31770  fourierdlem14  31792  fourierdlem19  31797  fourierdlem41  31819  fourierdlem42  31820  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem64  31842  fourierdlem74  31852  fourierdlem75  31853  fourierdlem81  31859  fourierdlem92  31870  fourierdlem97  31875  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  mvlladdd  32908  mvlraddd  32909  mvrladdd  32911  mvrraddd  32913  bj-lsub  34394  bj-bary1lem1  34403
  Copyright terms: Public domain W3C validator