Theorem chshii 30232

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

Syntax hints:   ∈ wcel 2106   S_ℋ csh 29933   C_ℋ cch 29934

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fv 6509  df-ov 7365  df-ch 30226

This theorem is referenced by:  chssii  30236  helsh  30250  h0elsh  30261  hhsscms  30283  hhssbnOLD  30284  chocunii  30306  shsleji  30375  shjshcli  30381  pjhthlem1  30396  pjhthlem2  30397  omlsii  30408  ococi  30410  pjoc1i  30436  chne0i  30458  chocini  30459  chjcli  30462  chsleji  30463  chseli  30464  chunssji  30472  chjcomi  30473  chub1i  30474  chlubi  30476  chlej1i  30478  chlej2i  30479  h1de2bi  30559  h1de2ctlem  30560  spansnpji  30583  spanunsni  30584  h1datomi  30586  pjoml2i  30590  qlaxr3i  30641  osumi  30647  osumcor2i  30649  spansnji  30651  spansnm0i  30655  nonbooli  30656  spansncvi  30657  5oai  30666  3oalem2  30668  3oalem5  30671  3oalem6  30672  pjaddii  30680  pjmulii  30682  pjss2i  30685  pjssmii  30686  pj0i  30698  pjocini  30703  pjjsi  30705  pjpythi  30727  mayete3i  30733  pjnmopi  31153  pjimai  31181  pjclem4  31204  pj3si  31212  sto1i  31241  stlei  31245  strlem1  31255  hatomici  31364  hatomistici  31367  atomli  31387  chirredlem3  31397  sumdmdii  31420  sumdmdlem  31423  sumdmdlem2  31424