Theorem resubcld 8312

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resubcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
resubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resubcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		resubcl 8195	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2146  (class class class)co 5865  ℝcr 7785   − cmin 8102

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-setind 4530  ax-resscn 7878  ax-1cn 7879  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-addcom 7886  ax-addass 7888  ax-distr 7890  ax-i2m1 7891  ax-0id 7894  ax-rnegex 7895  ax-cnre 7897

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-opab 4060  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-iota 5170  df-fun 5210  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-sub 8104  df-neg 8105

This theorem is referenced by:  ltsubadd  8363  lesubadd  8365  ltaddsub  8367  leaddsub  8369  lesub1  8387  lesub2  8388  ltsub1  8389  ltsub2  8390  lt2sub  8391  le2sub  8392  rereim  8517  ltmul1a  8522  cru  8533  lemul1a  8788  ztri3or  9269  lincmb01cmp  9974  iccf1o  9975  rebtwn2z  10225  qbtwnrelemcalc  10226  qbtwnre  10227  intfracq  10290  modqval  10294  modqlt  10303  modqsubdir  10363  ser3le  10488  expnbnd  10613  crre  10834  remullem  10848  recvguniqlem  10971  resqrexlemover  10987  resqrexlemcalc2  10992  resqrexlemcalc3  10993  resqrexlemnmsq  10994  resqrexlemnm  10995  resqrexlemcvg  10996  resqrexlemglsq  10999  resqrexlemga  11000  fzomaxdiflem  11089  caubnd2  11094  amgm2  11095  icodiamlt  11157  qdenre  11179  maxabslemab  11183  maxabslemlub  11184  maxltsup  11195  bdtrilem  11215  bdtri  11216  mulcn2  11288  reccn2ap  11289  climle  11310  climsqz  11311  climsqz2  11312  climcvg1nlem  11325  fsumle  11439  cvgratnnlembern  11499  cvgratnnlemsumlt  11504  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratnn  11507  efltim  11674  sin01bnd  11733  sin01gt0  11737  cos12dec  11743  uzwodc  12005  pythagtriplem12  12242  pythagtriplem14  12244  blss2ps  13486  blss2  13487  blssps  13507  blss  13508  ivthinclemlopn  13694  ivthinclemuopn  13696  dvcjbr  13752  reeff1oleme  13773  efltlemlt  13775  sin0pilem1  13782  tangtx  13839  cosordlem  13850  cosq34lt1  13851  cvgcmp2nlemabs  14350  iooref1o  14352  trilpolemlt1  14359  trirec0  14362  apdifflemf  14364