Theorem chshii 31154

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

Syntax hints:   ∈ wcel 2108   S_ℋ csh 30855   C_ℋ cch 30856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fv 6538  df-ov 7406  df-ch 31148

This theorem is referenced by:  chssii  31158  helsh  31172  h0elsh  31183  hhsscms  31205  hhssbnOLD  31206  chocunii  31228  shsleji  31297  shjshcli  31303  pjhthlem1  31318  pjhthlem2  31319  omlsii  31330  ococi  31332  pjoc1i  31358  chne0i  31380  chocini  31381  chjcli  31384  chsleji  31385  chseli  31386  chunssji  31394  chjcomi  31395  chub1i  31396  chlubi  31398  chlej1i  31400  chlej2i  31401  h1de2bi  31481  h1de2ctlem  31482  spansnpji  31505  spanunsni  31506  h1datomi  31508  pjoml2i  31512  qlaxr3i  31563  osumi  31569  osumcor2i  31571  spansnji  31573  spansnm0i  31577  nonbooli  31578  spansncvi  31579  5oai  31588  3oalem2  31590  3oalem5  31593  3oalem6  31594  pjaddii  31602  pjmulii  31604  pjss2i  31607  pjssmii  31608  pj0i  31620  pjocini  31625  pjjsi  31627  pjpythi  31649  mayete3i  31655  pjnmopi  32075  pjimai  32103  pjclem4  32126  pj3si  32134  sto1i  32163  stlei  32167  strlem1  32177  hatomici  32286  hatomistici  32289  atomli  32309  chirredlem3  32319  sumdmdii  32342  sumdmdlem  32345  sumdmdlem2  32346