Theorem chshii 28601

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

Syntax hints:   ∈ wcel 2157   S_ℋ csh 28302   C_ℋ cch 28303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rex 3093  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-opab 4904  df-xp 5316  df-cnv 5318  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fv 6107  df-ov 6879  df-ch 28595

This theorem is referenced by:  chssii  28605  helsh  28619  h0elsh  28630  hhsscms  28653  hhssbnOLD  28654  hhsshlOLD  28655  chocunii  28677  shsleji  28746  shjshcli  28752  pjhthlem1  28767  pjhthlem2  28768  omlsii  28779  ococi  28781  pjoc1i  28807  chne0i  28829  chocini  28830  chjcli  28833  chsleji  28834  chseli  28835  chunssji  28843  chjcomi  28844  chub1i  28845  chlubi  28847  chlej1i  28849  chlej2i  28850  h1de2bi  28930  h1de2ctlem  28931  spansnpji  28954  spanunsni  28955  h1datomi  28957  pjoml2i  28961  qlaxr3i  29012  osumi  29018  osumcor2i  29020  spansnji  29022  spansnm0i  29026  nonbooli  29027  spansncvi  29028  5oai  29037  3oalem2  29039  3oalem5  29042  3oalem6  29043  pjaddii  29051  pjmulii  29053  pjss2i  29056  pjssmii  29057  pj0i  29069  pjocini  29074  pjjsi  29076  pjpythi  29098  mayete3i  29104  pjnmopi  29524  pjimai  29552  pjclem4  29575  pj3si  29583  sto1i  29612  stlei  29616  strlem1  29626  hatomici  29735  hatomistici  29738  atomli  29758  chirredlem3  29768  sumdmdii  29791  sumdmdlem  29794  sumdmdlem2  29795