Theorem resubcld 8270

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 8153	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 409	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2135  (class class class)co 5836  ℝcr 7743   − 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  df-neg 8063

This theorem is referenced by:  ltsubadd  8321  lesubadd  8323  ltaddsub  8325  leaddsub  8327  lesub1  8345  lesub2  8346  ltsub1  8347  ltsub2  8348  lt2sub  8349  le2sub  8350  rereim  8475  ltmul1a  8480  cru  8491  lemul1a  8744  ztri3or  9225  lincmb01cmp  9930  iccf1o  9931  rebtwn2z  10180  qbtwnrelemcalc  10181  qbtwnre  10182  intfracq  10245  modqval  10249  modqlt  10258  modqsubdir  10318  ser3le  10443  expnbnd  10567  crre  10785  remullem  10799  recvguniqlem  10922  resqrexlemover  10938  resqrexlemcalc2  10943  resqrexlemcalc3  10944  resqrexlemnmsq  10945  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemglsq  10950  resqrexlemga  10951  fzomaxdiflem  11040  caubnd2  11045  amgm2  11046  icodiamlt  11108  qdenre  11130  maxabslemab  11134  maxabslemlub  11135  maxltsup  11146  bdtrilem  11166  bdtri  11167  mulcn2  11239  reccn2ap  11240  climle  11261  climsqz  11262  climsqz2  11263  climcvg1nlem  11276  fsumle  11390  cvgratnnlembern  11450  cvgratnnlemsumlt  11455  cvgratnnlemfm  11456  cvgratnnlemrate  11457  cvgratnn  11458  efltim  11625  sin01bnd  11684  sin01gt0  11688  cos12dec  11694  pythagtriplem12  12184  pythagtriplem14  12186  blss2ps  12947  blss2  12948  blssps  12968  blss  12969  ivthinclemlopn  13155  ivthinclemuopn  13157  dvcjbr  13213  reeff1oleme  13234  efltlemlt  13236  sin0pilem1  13243  tangtx  13300  cosordlem  13311  cosq34lt1  13312  cvgcmp2nlemabs  13745  iooref1o  13747  trilpolemlt1  13754  trirec0  13757  apdifflemf  13759