Theorem chshii 31387

Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
chshi.1	⊢ 𝐻 ∈ Cℋ

Assertion

Ref	Expression
chshii	⊢ 𝐻 ∈ Sℋ

Proof of Theorem chshii

Step	Hyp	Ref	Expression
1		chshi.1	. 2 ⊢ 𝐻 ∈ Cℋ
2		chsh 31384	. 2 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
3	1, 2	ax-mp 5	1 ⊢ 𝐻 ∈ Sℋ

Syntax hints:   ∈ wcel 2141   S_ℋ csh 31088   C_ℋ cch 31089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-xp 5649  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fv 6524  df-ov 7394  df-ch 31381

This theorem is referenced by:  chssii  31391  helsh  31405  h0elsh  31416  hhsscms  31438  hhssbnOLD  31439  chocunii  31461  shsleji  31530  shjshcli  31536  pjhthlem1  31551  pjhthlem2  31552  omlsii  31563  ococi  31565  pjoc1i  31591  chne0i  31613  chocini  31614  chjcli  31617  chsleji  31618  chseli  31619  chunssji  31627  chjcomi  31628  chub1i  31629  chlubi  31631  chlej1i  31633  chlej2i  31634  h1de2bi  31714  h1de2ctlem  31715  spansnpji  31738  spanunsni  31739  h1datomi  31741  pjoml2i  31745  qlaxr3i  31796  osumi  31802  osumcor2i  31804  spansnji  31806  spansnm0i  31810  nonbooli  31811  spansncvi  31812  5oai  31821  3oalem2  31823  3oalem5  31826  3oalem6  31827  pjaddii  31835  pjmulii  31837  pjss2i  31840  pjssmii  31841  pj0i  31853  pjocini  31858  pjjsi  31860  pjpythi  31882  mayete3i  31888  pjnmopi  32308  pjimai  32336  pjclem4  32359  pj3si  32367  sto1i  32396  stlei  32400  strlem1  32410  hatomici  32519  hatomistici  32522  atomli  32542  chirredlem3  32552  sumdmdii  32575  sumdmdlem  32578  sumdmdlem2  32579