Theorem chshii 31314

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

Syntax hints:   ∈ wcel 2114   S_ℋ csh 31015   C_ℋ cch 31016

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fv 6508  df-ov 7371  df-ch 31308

This theorem is referenced by:  chssii  31318  helsh  31332  h0elsh  31343  hhsscms  31365  hhssbnOLD  31366  chocunii  31388  shsleji  31457  shjshcli  31463  pjhthlem1  31478  pjhthlem2  31479  omlsii  31490  ococi  31492  pjoc1i  31518  chne0i  31540  chocini  31541  chjcli  31544  chsleji  31545  chseli  31546  chunssji  31554  chjcomi  31555  chub1i  31556  chlubi  31558  chlej1i  31560  chlej2i  31561  h1de2bi  31641  h1de2ctlem  31642  spansnpji  31665  spanunsni  31666  h1datomi  31668  pjoml2i  31672  qlaxr3i  31723  osumi  31729  osumcor2i  31731  spansnji  31733  spansnm0i  31737  nonbooli  31738  spansncvi  31739  5oai  31748  3oalem2  31750  3oalem5  31753  3oalem6  31754  pjaddii  31762  pjmulii  31764  pjss2i  31767  pjssmii  31768  pj0i  31780  pjocini  31785  pjjsi  31787  pjpythi  31809  mayete3i  31815  pjnmopi  32235  pjimai  32263  pjclem4  32286  pj3si  32294  sto1i  32323  stlei  32327  strlem1  32337  hatomici  32446  hatomistici  32449  atomli  32469  chirredlem3  32479  sumdmdii  32502  sumdmdlem  32505  sumdmdlem2  32506