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

Theorem pncan 9073
Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
pncan  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  -  B
)  =  A )

Proof of Theorem pncan
StepHypRef Expression
1 simpr 447 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
2 simpl 443 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  A  e.  CC )
31, 2addcomd 9030 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  A
)  =  ( A  +  B ) )
4 addcl 8835 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
5 subadd 9070 . . 3  |-  ( ( ( A  +  B
)  e.  CC  /\  B  e.  CC  /\  A  e.  CC )  ->  (
( ( A  +  B )  -  B
)  =  A  <->  ( B  +  A )  =  ( A  +  B ) ) )
64, 1, 2, 5syl3anc 1182 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  B )  -  B )  =  A  <-> 
( B  +  A
)  =  ( A  +  B ) ) )
73, 6mpbird 223 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  -  B
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756    - cmin 9053
This theorem is referenced by:  pncan2  9074  addsubass  9077  subid1  9084  nppcan2  9094  pncand  9174  nn1m1nn  9782  nnsub  9800  halfpm6th  9952  elnn0nn  10022  elz2  10056  zrevaddcl  10079  uzindOLD  10122  qrevaddcl  10354  irradd  10356  fzrev3  10865  fzrevral3  10884  fzval3  10927  seqf1olem1  11101  seqf1olem2  11102  subsq2  11227  bcp1nk  11345  bcp1m1  11348  bcpasc  11349  hashbclem  11406  wrdind  11493  shftlem  11579  shftval5  11589  isershft  12153  isercoll2  12158  fsump1  12235  fsumshft  12258  fsumtscopo  12276  fsumparts  12280  bcxmas  12310  isum1p  12316  climcndslem1  12324  geolim  12342  mertenslem2  12357  mertens  12358  ege2le3  12387  eftlub  12405  effsumlt  12407  eirrlem  12498  rpnnen2lem3  12511  rpnnen2lem11  12519  dvdsadd  12583  3dvds  12607  prmind2  12785  iserodd  12904  fldivp1  12961  prmpwdvds  12967  pockthlem  12968  prmreclem4  12982  prmreclem6  12984  4sqlem11  13018  vdwapun  13037  ramub1lem1  13089  ramcl  13092  1259lem4  13148  1259prm  13150  2503lem2  13152  2503prm  13154  4001lem3  13157  4001prm  13159  efgsval2  15058  efgsrel  15059  pcoass  18538  shft2rab  18883  ovolicc2lem4  18895  uniioombllem3  18956  uniioombllem4  18957  dvexp  19318  dvfsumlem1  19389  degltp1le  19475  ply1divex  19538  plyaddlem1  19611  plymullem1  19612  dvply1  19680  dvply2g  19681  vieta1lem2  19707  aaliou3lem7  19745  dvradcnv  19813  pserdvlem2  19820  abssinper  19902  eff1o  19927  advlogexp  20018  atantayl3  20251  leibpilem1  20252  leibpilem2  20253  log2cnv  20256  log2tlbnd  20257  log2ub  20261  birthday  20265  emcllem2  20306  harmonicbnd4  20320  wilthlem2  20323  basellem8  20341  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  chpp1  20409  ppiublem2  20458  ppiub  20459  chtublem  20466  chtub  20467  perfectlem1  20484  perfectlem2  20485  perfect  20486  bcp1ctr  20534  bposlem6  20544  bposlem8  20546  lgsvalmod  20570  lgseisen  20608  lgsquadlem1  20609  lgsquad2lem1  20613  2sqlem10  20629  rplogsumlem1  20649  selberg2lem  20715  logdivbnd  20721  pntrsumo1  20730  pntpbnd2  20752  gxadd  20958  lnfn0i  22638  subfacp1lem5  23730  subfacp1lem6  23731  subfacval2  23733  subfaclim  23734  cvmliftlem7  23837  cvmliftlem10  23840  eupap1  23915  eupath2lem3  23918  elfzp1b  24027  bpolydiflem  24861  fsumkthpow  24863  bpoly3  24865  fsumcube  24867  itg2addnc  25005  mslb1  25710  2wsms  25711  fdc  26558  mettrifi  26576  heiborlem4  26641  heiborlem6  26643  lzenom  26952  2nn0ind  27133  jm2.17a  27150  jm2.17b  27151  jm2.17c  27152  stoweidlem17  27869  stoweidlem34  27886
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-po 4330  df-so 4331  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-riota 6320  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-ltxr 8888  df-sub 9055
  Copyright terms: Public domain W3C validator