Theorem subcld 8639

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 8527	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A - B ) e. CC )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   CCcc 8178   - cmin 8499

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-setind 4684  ax-resscn 8272  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-addcom 8280  ax-addass 8282  ax-distr 8284  ax-i2m1 8285  ax-0id 8288  ax-rnegex 8289  ax-cnre 8291

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-sub 8501

This theorem is used by:  pnpncand  8703  kcnktkm1cn  8712  muleqadd  9001  ofnegsub  9295  peano2zm  9687  peano5uzti  9759  modqmuladdnn0  10820  modsumfzodifsn  10848  bcm1n  11223  hashfz  11278  hashfzo  11279  hashf1lem2  11302  hashf1  11303  ccatswrd  11458  pfxccatin12lem2  11519  shftfvalg  11599  ovshftex  11600  shftfibg  11601  shftfval  11602  shftdm  11603  shftfib  11604  shftval  11606  2shfti  11612  crre  11638  remim  11641  remullem  11652  resqrexlemover  11792  resqrexlemcalc1  11796  abssubne0  11874  abs3lem  11894  caubnd2  11900  maxabslemlub  11990  maxabslemval  11991  maxcl  11993  minabs  12020  bdtrilem  12024  bdtri  12025  climuni  12078  mulcn2  12097  reccn2ap  12098  cn1lem  12099  climcvg1nlem  12134  fsumparts  12256  arisum2  12285  geosergap  12292  geo2sum2  12301  geoisum1c  12306  cvgratnnlemrate  12316  sinval  12488  sinf  12490  tanval2ap  12499  tanval3ap  12500  sinneg  12512  efival  12518  cos12dec  12554  bitsinv1lem  12747  pythagtriplem1  13067  pythagtriplem14  13079  pythagtriplem16  13081  pythagtriplem17  13082  dvdsprmpweqle  13139  4sqlem5  13184  mul4sqlem  13195  4sqlem17  13209  gzsumshift  14233  addcncntoplem  15753  mulcncflem  15799  cnopnap  15803  limcimolemlt  15856  limcimo  15857  cnplimclemle  15860  limccnp2lem  15868  dvlemap  15872  dvconst  15886  dvid  15887  dvconstre  15888  dvidre  15889  dvconstss  15890  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  dveflem  15918  dvef  15919  sin0pilem1  15974  ptolemy  16017  tangtx  16031  cosq34lt1  16043  pellexlem2  16191  lgsdirprm  16319  gausslemma2dlem1a  16343  clwwlknonex2lem1  16844  dichmul0orlem7  16925  qdencn  17238  trirec0  17260  apdifflemf  17262  apdifflemr  17263  apdiff  17264  qdiff  17265