Theorem chshii 29490

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

Syntax hints:   ∈ wcel 2108   S_ℋ csh 29191   C_ℋ cch 29192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fv 6426  df-ov 7258  df-ch 29484

This theorem is referenced by:  chssii  29494  helsh  29508  h0elsh  29519  hhsscms  29541  hhssbnOLD  29542  chocunii  29564  shsleji  29633  shjshcli  29639  pjhthlem1  29654  pjhthlem2  29655  omlsii  29666  ococi  29668  pjoc1i  29694  chne0i  29716  chocini  29717  chjcli  29720  chsleji  29721  chseli  29722  chunssji  29730  chjcomi  29731  chub1i  29732  chlubi  29734  chlej1i  29736  chlej2i  29737  h1de2bi  29817  h1de2ctlem  29818  spansnpji  29841  spanunsni  29842  h1datomi  29844  pjoml2i  29848  qlaxr3i  29899  osumi  29905  osumcor2i  29907  spansnji  29909  spansnm0i  29913  nonbooli  29914  spansncvi  29915  5oai  29924  3oalem2  29926  3oalem5  29929  3oalem6  29930  pjaddii  29938  pjmulii  29940  pjss2i  29943  pjssmii  29944  pj0i  29956  pjocini  29961  pjjsi  29963  pjpythi  29985  mayete3i  29991  pjnmopi  30411  pjimai  30439  pjclem4  30462  pj3si  30470  sto1i  30499  stlei  30503  strlem1  30513  hatomici  30622  hatomistici  30625  atomli  30645  chirredlem3  30655  sumdmdii  30678  sumdmdlem  30681  sumdmdlem2  30682