Theorem chshii 29004

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

Syntax hints:   ∈ wcel 2114   S_ℋ csh 28705   C_ℋ cch 28706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fv 6363  df-ov 7159  df-ch 28998

This theorem is referenced by:  chssii  29008  helsh  29022  h0elsh  29033  hhsscms  29055  hhssbnOLD  29056  chocunii  29078  shsleji  29147  shjshcli  29153  pjhthlem1  29168  pjhthlem2  29169  omlsii  29180  ococi  29182  pjoc1i  29208  chne0i  29230  chocini  29231  chjcli  29234  chsleji  29235  chseli  29236  chunssji  29244  chjcomi  29245  chub1i  29246  chlubi  29248  chlej1i  29250  chlej2i  29251  h1de2bi  29331  h1de2ctlem  29332  spansnpji  29355  spanunsni  29356  h1datomi  29358  pjoml2i  29362  qlaxr3i  29413  osumi  29419  osumcor2i  29421  spansnji  29423  spansnm0i  29427  nonbooli  29428  spansncvi  29429  5oai  29438  3oalem2  29440  3oalem5  29443  3oalem6  29444  pjaddii  29452  pjmulii  29454  pjss2i  29457  pjssmii  29458  pj0i  29470  pjocini  29475  pjjsi  29477  pjpythi  29499  mayete3i  29505  pjnmopi  29925  pjimai  29953  pjclem4  29976  pj3si  29984  sto1i  30013  stlei  30017  strlem1  30027  hatomici  30136  hatomistici  30139  atomli  30159  chirredlem3  30169  sumdmdii  30192  sumdmdlem  30195  sumdmdlem2  30196