Theorem pncan 9753

Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)

Assertion

Ref	Expression
pncan

Proof of Theorem pncan

Step	Hyp	Ref	Expression
1		simpr 461	. . 3
2		simpl 457	. . 3
3	1, 2	addcomd 9708	. 2
4		addcl 9501	. . 3
5		subadd 9750	. . 3
6	4, 1, 2, 5	syl3anc 1219	. 2
7	3, 6	mpbird 232	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1758  (class class class)co 6222  cc 9417  caddc 9422  cmin 9732

This theorem is referenced by:  pncan2  9754  addsubass  9757  pncan3oi  9763  subid1  9766  nppcan2  9777  pncand  9857  nn1m1nn  10480  nnsub  10498  elnn0nn  10760  elz2  10801  zrevaddcl  10828  uzindOLD  10874  qrevaddcl  11114  irradd  11116  fzrev3  11667  elfzp1b  11682  fzrevral3  11691  fzval3  11750  seqf1olem1  12002  seqf1olem2  12003  subsq2  12131  bcp1nk  12250  bcp1m1  12253  bcpasc  12254  hashbclem  12363  wrdind  12529  wrd2ind  12530  shftlem  12715  shftval5  12725  isershft  13299  isercoll2  13304  fsump1  13381  mptfzshft  13403  fsumtscopo  13423  fsumparts  13427  bcxmas  13456  isum1p  13462  climcndslem1  13470  geolim  13488  mertenslem2  13503  mertens  13504  eftlub  13551  effsumlt  13553  eirrlem  13644  dvdsadd  13729  3dvds  13754  prmind2  13932  iserodd  14060  fldivp1  14117  prmpwdvds  14123  pockthlem  14124  prmreclem4  14138  prmreclem6  14140  4sqlem11  14174  vdwapun  14193  ramub1lem1  14245  ramcl  14248  1259lem4  14316  1259prm  14318  2503lem2  14320  2503prm  14322  4001lem3  14325  4001prm  14327  efgsval2  16391  efgsrel  16392  pcoass  20995  shft2rab  21390  ovolicc2lem4  21402  uniioombllem3  21465  uniioombllem4  21466  dvexp  21827  dvfsumlem1  21898  degltp1le  21944  ply1divex  22008  plyaddlem1  22081  plymullem1  22082  dvply1  22150  dvply2g  22151  vieta1lem2  22177  aaliou3lem7  22215  dvradcnv  22286  pserdvlem2  22293  abssinper  22380  eff1o  22405  advlogexp  22500  atantayl3  22734  leibpilem1  22735  leibpilem2  22736  log2tlbnd  22740  log2ub  22744  birthday  22748  emcllem2  22790  harmonicbnd4  22804  wilthlem2  22807  basellem8  22825  ppiprm  22889  ppinprm  22890  chtprm  22891  chtnprm  22892  chpp1  22893  ppiublem2  22942  ppiub  22943  chtub  22951  perfectlem1  22968  perfectlem2  22969  perfect  22970  bcp1ctr  23018  bposlem6  23028  bposlem8  23030  lgsvalmod  23054  lgseisen  23092  lgsquadlem1  23093  lgsquad2lem1  23097  2sqlem10  23113  rplogsumlem1  23133  selberg2lem  23199  logdivbnd  23205  pntrsumo1  23214  pntpbnd2  23236  eupap1  24066  eupath2lem3  24069  gxadd  24231  lnfn0i  25915  subfacp1lem5  27528  subfacp1lem6  27529  subfacval2  27531  subfaclim  27532  cvmliftlem7  27636  cvmliftlem10  27639  fsumkthpow  28655  mblfinlem2  28889  itg2addnclem3  28905  fdc  29101  mettrifi  29113  heiborlem4  29173  heiborlem6  29175  lzenom  29568  2nn0ind  29746  jm2.17a  29763  jm2.17b  29764  jm2.17c  29765  fouriersw  30761  wlklenfislenpm1  31161  wlkiswwlk1  31201  wwlknext  31233  clwwlkf1  31335  cshwlemma1  31366  extwwlkfablem2  31548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505  ax-resscn 9476  ax-1cn 9477  ax-icn 9478  ax-addcl 9479  ax-addrcl 9480  ax-mulcl 9481  ax-mulrcl 9482  ax-mulcom 9483  ax-addass 9484  ax-mulass 9485  ax-distr 9486  ax-i2m1 9487  ax-1ne0 9488  ax-1rid 9489  ax-rnegex 9490  ax-rrecex 9491  ax-cnre 9492  ax-pre-lttri 9493  ax-pre-lttrn 9494  ax-pre-ltadd 9495

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-mpt 4469  df-id 4753  df-po 4758  df-so 4759  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6183  df-ov 6225  df-oprab 6226  df-mpt2 6227  df-er 7235  df-en 7445  df-dom 7446  df-sdom 7447  df-pnf 9557  df-mnf 9558  df-ltxr 9560  df-sub 9734