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

Theorem pncand 9725
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 9621 . 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 1369    e. wcel 1756  (class class class)co 6096   CCcc 9285    + caddc 9290    - cmin 9600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-po 4646  df-so 4647  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-pnf 9425  df-mnf 9426  df-ltxr 9428  df-sub 9602
This theorem is referenced by:  pncan1  9777  icoshftf1o  11413  xov1plusxeqvd  11436  zesq  11992  brfi1indlem  12223  ccatval3  12283  wrdlenccats1lenm1  12310  fsumrev2  13254  binom1dif  13301  sadcp1  13656  smupp1  13681  hashdvds  13855  pythagtriplem4  13891  pythagtriplem6  13893  pythagtriplem7  13894  pythagtriplem12  13898  pythagtriplem14  13900  pcqdiv  13929  mulgdirlem  15656  blhalf  19985  pjthlem1  20929  ovolicopnf  21012  i1faddlem  21176  itg1addlem4  21182  ftc1lem4  21516  aaliou3lem8  21816  taylthlem2  21844  ulmshft  21860  efif1olem2  22004  efif1olem4  22006  quart1lem  22255  asinsin  22292  efiatan2  22317  logdiflbnd  22393  harmonicbnd4  22409  ftalem1  22415  ftalem2  22416  bcctr  22619  pcbcctr  22620  bcp1ctr  22623  2sqblem  22721  mulog2sumlem1  22788  mulog2sumlem3  22790  pntrlog2bndlem2  22832  pntrlog2bndlem4  22834  pntrlog2bndlem5  22835  pntrlog2bndlem6  22837  colinearalglem4  23160  axpaschlem  23191  eupatrl  23594  pjhthlem1  24799  dya2icoseg  26697  iwrdsplit  26775  fibp1  26789  ballotlemfc0  26880  ballotlemfcc  26881  ballotlemsgt1  26898  ballotlemsel1i  26900  ballotlemsima  26903  ballotlem1ri  26922  eluzmn  26940  signstfvn  26975  lgamgulmlem2  27021  lgamcvg2  27046  relgamcl  27053  pnpncand  27399  fprodp1  27484  fprodshft  27492  risefacp1  27537  fallfacp1  27538  bpolydiflem  28202  fsumcube  28208  sin2h  28427  itg2addnclem  28448  itg2addnclem3  28450  ftc1cnnclem  28470  areacirclem4  28492  ssbnd  28692  jm2.19lem4  29346  jm2.23  29350  jm3.1lem1  29371  itgpowd  29595  climinf  29784  stoweidlem17  29817  wallispilem4  29868  wallispilem5  29869  stirlinglem1  29874  stirlinglem5  29878  stirlinglem6  29879  stirlinglem10  29883  wwlknimp  30326  wlklniswwlkn2  30339  wwlknred  30360  wwlknredwwlkn  30363  clwlkisclwwlklem1  30454  clwlkisclwwlklem0  30455  clwwlkf  30461  wwlkext2clwwlk  30470  wwlkextproplem2  30566  rusgra0edg  30578  numclwwlk2lem1  30700  numclwlk2lem2f  30701  mvlladdd  31120  mvlraddd  31121  mvrladdd  31123  mvrraddd  31125  bj-lsub  32596  bj-bary1lem1  32605
  Copyright terms: Public domain W3C validator