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

Theorem pncan 9817
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 459 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  B  e.  CC )
2 simpl 455 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  A  e.  CC )
31, 2addcomd 9771 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( B  +  A
)  =  ( A  +  B ) )
4 addcl 9563 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
5 subadd 9814 . . 3  |-  ( ( ( A  +  B
)  e.  CC  /\  B  e.  CC  /\  A  e.  CC )  ->  (
( ( A  +  B )  -  B
)  =  A  <->  ( B  +  A )  =  ( A  +  B ) ) )
64, 1, 2, 5syl3anc 1226 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( ( A  +  B )  -  B )  =  A  <-> 
( B  +  A
)  =  ( A  +  B ) ) )
73, 6mpbird 232 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  -  B
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479    + caddc 9484    - cmin 9796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622  df-sub 9798
This theorem is referenced by:  pncan2  9818  addsubass  9821  pncan3oi  9827  subid1  9830  nppcan2  9841  pncand  9923  nn1m1nn  10551  nnsub  10570  elnn0nn  10834  elz2  10877  zrevaddcl  10905  uzindOLD  10953  qrevaddcl  11205  irradd  11207  fzrev3  11749  elfzp1b  11759  fzrevral3  11769  fzval3  11866  seqf1olem1  12128  seqf1olem2  12129  subsq2  12258  bcp1nk  12377  bcp1m1  12380  bcpasc  12381  hashbclem  12485  wrdind  12693  wrd2ind  12694  2cshwcshw  12784  shftlem  12983  shftval5  12993  isershft  13568  isercoll2  13573  fsump1  13653  mptfzshft  13675  telfsumo  13698  fsumparts  13702  bcxmas  13729  isum1p  13735  geolim  13761  mertenslem2  13776  mertens  13777  eftlub  13926  effsumlt  13928  eirrlem  14019  dvdsadd  14108  prmind2  14312  iserodd  14443  fldivp1  14500  prmpwdvds  14506  pockthlem  14507  prmreclem4  14521  prmreclem6  14523  4sqlem11  14557  vdwapun  14576  ramub1lem1  14628  ramcl  14631  efgsval2  16950  efgsrel  16951  pcoass  21690  shft2rab  22085  uniioombllem3  22160  uniioombllem4  22161  dvexp  22522  dvfsumlem1  22593  degltp1le  22639  ply1divex  22703  plyaddlem1  22776  plymullem1  22777  dvply1  22846  dvply2g  22847  vieta1lem2  22873  aaliou3lem7  22911  dvradcnv  22982  pserdvlem2  22989  abssinper  23077  advlogexp  23204  atantayl3  23467  leibpilem1  23468  leibpilem2  23469  emcllem2  23524  harmonicbnd4  23538  wilthlem2  23541  basellem8  23559  ppiprm  23623  ppinprm  23624  chtprm  23625  chtnprm  23626  chpp1  23627  chtub  23685  perfectlem1  23702  perfectlem2  23703  perfect  23704  bcp1ctr  23752  lgsvalmod  23788  lgseisen  23826  lgsquadlem1  23827  lgsquad2lem1  23831  2sqlem10  23847  rplogsumlem1  23867  selberg2lem  23933  logdivbnd  23939  pntrsumo1  23948  pntpbnd2  23970  wlklenvm1  24734  wlkiswwlk1  24892  wwlknext  24926  clwwlkf1  24998  eupap1  25178  eupath2lem3  25181  extwwlkfablem2  25280  gxadd  25475  subfacp1lem5  28892  subfacp1lem6  28893  subfacval2  28895  subfaclim  28896  cvmliftlem7  29000  cvmliftlem10  29003  fsumkthpow  30046  mblfinlem2  30292  itg2addnclem3  30308  fdc  30478  mettrifi  30490  heiborlem4  30550  heiborlem6  30552  lzenom  30942  2nn0ind  31120  jm2.17a  31137  jm2.17b  31138  jm2.17c  31139
  Copyright terms: Public domain W3C validator