Theorem chshii 31560

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

Syntax hints:   ∈ wcel 2143   S_ℋ csh 31261   C_ℋ cch 31262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fv 6546  df-ov 7415  df-ch 31554

This theorem is referenced by:  chssii  31564  helsh  31578  h0elsh  31589  hhsscms  31611  hhssbnOLD  31612  chocunii  31634  shsleji  31703  shjshcli  31709  pjhthlem1  31724  pjhthlem2  31725  omlsii  31736  ococi  31738  pjoc1i  31764  chne0i  31786  chocini  31787  chjcli  31790  chsleji  31791  chseli  31792  chunssji  31800  chjcomi  31801  chub1i  31802  chlubi  31804  chlej1i  31806  chlej2i  31807  h1de2bi  31887  h1de2ctlem  31888  spansnpji  31911  spanunsni  31912  h1datomi  31914  pjoml2i  31918  qlaxr3i  31969  osumi  31975  osumcor2i  31977  spansnji  31979  spansnm0i  31983  nonbooli  31984  spansncvi  31985  5oai  31994  3oalem2  31996  3oalem5  31999  3oalem6  32000  pjaddii  32008  pjmulii  32010  pjss2i  32013  pjssmii  32014  pj0i  32026  pjocini  32031  pjjsi  32033  pjpythi  32055  mayete3i  32061  pjnmopi  32481  pjimai  32509  pjclem4  32532  pj3si  32540  sto1i  32569  stlei  32573  strlem1  32583  hatomici  32692  hatomistici  32695  atomli  32715  chirredlem3  32725  sumdmdii  32748  sumdmdlem  32751  sumdmdlem2  32752