Theorem subcld 7990

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

Syntax hints:   -> wi 4   e. wcel 1461  (class class class)co 5726   CCcc 7539   - cmin 7850

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-setind 4410  ax-resscn 7631  ax-1cn 7632  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-iota 5044  df-fun 5081  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-sub 7852

This theorem is referenced by:  pnpncand  8050  kcnktkm1cn  8058  muleqadd  8336  peano2zm  8990  peano5uzti  9057  modqmuladdnn0  10028  modsumfzodifsn  10056  hashfz  10454  hashfzo  10455  shftfvalg  10477  ovshftex  10478  shftfibg  10479  shftfval  10480  shftdm  10481  shftfib  10482  shftval  10484  2shfti  10490  crre  10516  remim  10519  remullem  10530  resqrexlemover  10668  resqrexlemcalc1  10672  abssubne0  10749  abs3lem  10769  caubnd2  10775  maxabslemlub  10865  maxabslemval  10866  maxcl  10868  minabs  10893  bdtrilem  10896  bdtri  10897  climuni  10948  mulcn2  10967  reccn2ap  10968  cn1lem  10969  climcvg1nlem  11004  fsumparts  11125  arisum2  11154  geosergap  11161  geo2sum2  11170  geoisum1c  11175  cvgratnnlemrate  11185  sinval  11254  sinf  11256  tanval2ap  11265  tanval3ap  11266  sinneg  11278  efival  11284  addcncntoplem  12531  mulcncflem  12570  limcimolemlt  12583  limcimo  12584  cnplimclemle  12587  limccnp2lem  12595  dvlemap  12598  dvconst  12610  dvid  12611  dvcnp2cntop  12612  dvaddxxbr  12614  qdencn  12903