Theorem chshii 31822

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 31819	. 2 ⊢ (𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
3	1, 2	ax-mp 5	1 ⊢ 𝐻 ∈ Sℋ

This proof depends on syntax axioms:   ∈ wcel 2145   S_ℋ csh 31523   C_ℋ cch 31524

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fv 6545  df-ov 7421  df-ch 31816

This theorem is used by:  chssii  31826  helsh  31840  h0elsh  31851  hhsscms  31873  hhssbnOLD  31874  chocunii  31896  shsleji  31965  shjshcli  31971  pjhthlem1  31986  pjhthlem2  31987  omlsii  31998  ococi  32000  pjoc1i  32026  chne0i  32048  chocini  32049  chjcli  32052  chsleji  32053  chseli  32054  chunssji  32062  chjcomi  32063  chub1i  32064  chlubi  32066  chlej1i  32068  chlej2i  32069  h1de2bi  32149  h1de2ctlem  32150  spansnpji  32173  spanunsni  32174  h1datomi  32176  pjoml2i  32180  qlaxr3i  32231  osumi  32237  osumcor2i  32239  spansnji  32241  spansnm0i  32245  nonbooli  32246  spansncvi  32247  5oai  32256  3oalem2  32258  3oalem5  32261  3oalem6  32262  pjaddii  32270  pjmulii  32272  pjss2i  32275  pjssmii  32276  pj0i  32288  pjocini  32293  pjjsi  32295  pjpythi  32317  mayete3i  32323  pjnmopi  32743  pjimai  32771  pjclem4  32794  pj3si  32802  sto1i  32831  stlei  32835  strlem1  32845  hatomici  32954  hatomistici  32957  atomli  32977  chirredlem3  32987  sumdmdii  33010  sumdmdlem  33013  sumdmdlem2  33014