Theorem subcld 8200

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

Syntax hints:   -> wi 4   e. wcel 2135  (class class class)co 5836   CCcc 7742   - cmin 8060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-setind 4508  ax-resscn 7836  ax-1cn 7837  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-addcom 7844  ax-addass 7846  ax-distr 7848  ax-i2m1 7849  ax-0id 7852  ax-rnegex 7853  ax-cnre 7855

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2723  df-sbc 2947  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-iota 5147  df-fun 5184  df-fv 5190  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-sub 8062

This theorem is referenced by:  pnpncand  8264  kcnktkm1cn  8272  muleqadd  8556  peano2zm  9220  peano5uzti  9290  modqmuladdnn0  10293  modsumfzodifsn  10321  hashfz  10723  hashfzo  10724  shftfvalg  10746  ovshftex  10747  shftfibg  10748  shftfval  10749  shftdm  10750  shftfib  10751  shftval  10753  2shfti  10759  crre  10785  remim  10788  remullem  10799  resqrexlemover  10938  resqrexlemcalc1  10942  abssubne0  11019  abs3lem  11039  caubnd2  11045  maxabslemlub  11135  maxabslemval  11136  maxcl  11138  minabs  11163  bdtrilem  11166  bdtri  11167  climuni  11220  mulcn2  11239  reccn2ap  11240  cn1lem  11241  climcvg1nlem  11276  fsumparts  11397  arisum2  11426  geosergap  11433  geo2sum2  11442  geoisum1c  11447  cvgratnnlemrate  11457  sinval  11629  sinf  11631  tanval2ap  11640  tanval3ap  11641  sinneg  11653  efival  11659  cos12dec  11694  pythagtriplem1  12174  pythagtriplem14  12186  pythagtriplem16  12188  pythagtriplem17  12189  dvdsprmpweqle  12245  addcncntoplem  13092  mulcncflem  13131  cnopnap  13135  limcimolemlt  13174  limcimo  13175  cnplimclemle  13178  limccnp2lem  13186  dvlemap  13190  dvconst  13202  dvid  13203  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvrecap  13218  dveflem  13228  dvef  13229  sin0pilem1  13243  ptolemy  13286  tangtx  13300  cosq34lt1  13312  qdencn  13740  trirec0  13757  apdifflemf  13759  apdifflemr  13760  apdiff  13761