Theorem chshii 31213

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

Syntax hints:   ∈ wcel 2109   S_ℋ csh 30914   C_ℋ cch 30915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fv 6544  df-ov 7413  df-ch 31207

This theorem is referenced by:  chssii  31217  helsh  31231  h0elsh  31242  hhsscms  31264  hhssbnOLD  31265  chocunii  31287  shsleji  31356  shjshcli  31362  pjhthlem1  31377  pjhthlem2  31378  omlsii  31389  ococi  31391  pjoc1i  31417  chne0i  31439  chocini  31440  chjcli  31443  chsleji  31444  chseli  31445  chunssji  31453  chjcomi  31454  chub1i  31455  chlubi  31457  chlej1i  31459  chlej2i  31460  h1de2bi  31540  h1de2ctlem  31541  spansnpji  31564  spanunsni  31565  h1datomi  31567  pjoml2i  31571  qlaxr3i  31622  osumi  31628  osumcor2i  31630  spansnji  31632  spansnm0i  31636  nonbooli  31637  spansncvi  31638  5oai  31647  3oalem2  31649  3oalem5  31652  3oalem6  31653  pjaddii  31661  pjmulii  31663  pjss2i  31666  pjssmii  31667  pj0i  31679  pjocini  31684  pjjsi  31686  pjpythi  31708  mayete3i  31714  pjnmopi  32134  pjimai  32162  pjclem4  32185  pj3si  32193  sto1i  32222  stlei  32226  strlem1  32236  hatomici  32345  hatomistici  32348  atomli  32368  chirredlem3  32378  sumdmdii  32401  sumdmdlem  32404  sumdmdlem2  32405