Theorem chshii 31313

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

Syntax hints:   ∈ wcel 2114   S_ℋ csh 31014   C_ℋ cch 31015

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fv 6500  df-ov 7363  df-ch 31307

This theorem is referenced by:  chssii  31317  helsh  31331  h0elsh  31342  hhsscms  31364  hhssbnOLD  31365  chocunii  31387  shsleji  31456  shjshcli  31462  pjhthlem1  31477  pjhthlem2  31478  omlsii  31489  ococi  31491  pjoc1i  31517  chne0i  31539  chocini  31540  chjcli  31543  chsleji  31544  chseli  31545  chunssji  31553  chjcomi  31554  chub1i  31555  chlubi  31557  chlej1i  31559  chlej2i  31560  h1de2bi  31640  h1de2ctlem  31641  spansnpji  31664  spanunsni  31665  h1datomi  31667  pjoml2i  31671  qlaxr3i  31722  osumi  31728  osumcor2i  31730  spansnji  31732  spansnm0i  31736  nonbooli  31737  spansncvi  31738  5oai  31747  3oalem2  31749  3oalem5  31752  3oalem6  31753  pjaddii  31761  pjmulii  31763  pjss2i  31766  pjssmii  31767  pj0i  31779  pjocini  31784  pjjsi  31786  pjpythi  31808  mayete3i  31814  pjnmopi  32234  pjimai  32262  pjclem4  32285  pj3si  32293  sto1i  32322  stlei  32326  strlem1  32336  hatomici  32445  hatomistici  32448  atomli  32468  chirredlem3  32478  sumdmdii  32501  sumdmdlem  32504  sumdmdlem2  32505