Theorem subcld 8337

Description: Closure 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
subcld	|- ( ph -> ( A - B ) e. CC )

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 |- ( ph -> A e. CC )
2		pncand.2	. 2 |- ( ph -> B e. CC )
3		subcl 8225	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 2167  (class class class)co 5922   CCcc 7877   - cmin 8197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-setind 4573  ax-resscn 7971  ax-1cn 7972  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-iota 5219  df-fun 5260  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-sub 8199

This theorem is referenced by:  pnpncand  8401  kcnktkm1cn  8409  muleqadd  8695  ofnegsub  8989  peano2zm  9364  peano5uzti  9434  modqmuladdnn0  10460  modsumfzodifsn  10488  hashfz  10913  hashfzo  10914  shftfvalg  10983  ovshftex  10984  shftfibg  10985  shftfval  10986  shftdm  10987  shftfib  10988  shftval  10990  2shfti  10996  crre  11022  remim  11025  remullem  11036  resqrexlemover  11175  resqrexlemcalc1  11179  abssubne0  11256  abs3lem  11276  caubnd2  11282  maxabslemlub  11372  maxabslemval  11373  maxcl  11375  minabs  11401  bdtrilem  11404  bdtri  11405  climuni  11458  mulcn2  11477  reccn2ap  11478  cn1lem  11479  climcvg1nlem  11514  fsumparts  11635  arisum2  11664  geosergap  11671  geo2sum2  11680  geoisum1c  11685  cvgratnnlemrate  11695  sinval  11867  sinf  11869  tanval2ap  11878  tanval3ap  11879  sinneg  11891  efival  11897  cos12dec  11933  pythagtriplem1  12434  pythagtriplem14  12446  pythagtriplem16  12448  pythagtriplem17  12449  dvdsprmpweqle  12506  4sqlem5  12551  mul4sqlem  12562  4sqlem17  12576  addcncntoplem  14797  mulcncflem  14843  cnopnap  14847  limcimolemlt  14900  limcimo  14901  cnplimclemle  14904  limccnp2lem  14912  dvlemap  14916  dvconst  14930  dvid  14931  dvconstre  14932  dvidre  14933  dvconstss  14934  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  dveflem  14962  dvef  14963  sin0pilem1  15017  ptolemy  15060  tangtx  15074  cosq34lt1  15086  lgsdirprm  15275  gausslemma2dlem1a  15299  qdencn  15671  trirec0  15688  apdifflemf  15690  apdifflemr  15691  apdiff  15692