Theorem chshii 29010

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

Syntax hints:   ∈ wcel 2111   S_ℋ csh 28711   C_ℋ cch 28712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fv 6332  df-ov 7138  df-ch 29004

This theorem is referenced by:  chssii  29014  helsh  29028  h0elsh  29039  hhsscms  29061  hhssbnOLD  29062  chocunii  29084  shsleji  29153  shjshcli  29159  pjhthlem1  29174  pjhthlem2  29175  omlsii  29186  ococi  29188  pjoc1i  29214  chne0i  29236  chocini  29237  chjcli  29240  chsleji  29241  chseli  29242  chunssji  29250  chjcomi  29251  chub1i  29252  chlubi  29254  chlej1i  29256  chlej2i  29257  h1de2bi  29337  h1de2ctlem  29338  spansnpji  29361  spanunsni  29362  h1datomi  29364  pjoml2i  29368  qlaxr3i  29419  osumi  29425  osumcor2i  29427  spansnji  29429  spansnm0i  29433  nonbooli  29434  spansncvi  29435  5oai  29444  3oalem2  29446  3oalem5  29449  3oalem6  29450  pjaddii  29458  pjmulii  29460  pjss2i  29463  pjssmii  29464  pj0i  29476  pjocini  29481  pjjsi  29483  pjpythi  29505  mayete3i  29511  pjnmopi  29931  pjimai  29959  pjclem4  29982  pj3si  29990  sto1i  30019  stlei  30023  strlem1  30033  hatomici  30142  hatomistici  30145  atomli  30165  chirredlem3  30175  sumdmdii  30198  sumdmdlem  30201  sumdmdlem2  30202