Theorem chshii 30913

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

Syntax hints:   ∈ wcel 2105   S_ℋ csh 30614   C_ℋ cch 30615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fv 6551  df-ov 7415  df-ch 30907

This theorem is referenced by:  chssii  30917  helsh  30931  h0elsh  30942  hhsscms  30964  hhssbnOLD  30965  chocunii  30987  shsleji  31056  shjshcli  31062  pjhthlem1  31077  pjhthlem2  31078  omlsii  31089  ococi  31091  pjoc1i  31117  chne0i  31139  chocini  31140  chjcli  31143  chsleji  31144  chseli  31145  chunssji  31153  chjcomi  31154  chub1i  31155  chlubi  31157  chlej1i  31159  chlej2i  31160  h1de2bi  31240  h1de2ctlem  31241  spansnpji  31264  spanunsni  31265  h1datomi  31267  pjoml2i  31271  qlaxr3i  31322  osumi  31328  osumcor2i  31330  spansnji  31332  spansnm0i  31336  nonbooli  31337  spansncvi  31338  5oai  31347  3oalem2  31349  3oalem5  31352  3oalem6  31353  pjaddii  31361  pjmulii  31363  pjss2i  31366  pjssmii  31367  pj0i  31379  pjocini  31384  pjjsi  31386  pjpythi  31408  mayete3i  31414  pjnmopi  31834  pjimai  31862  pjclem4  31885  pj3si  31893  sto1i  31922  stlei  31926  strlem1  31936  hatomici  32045  hatomistici  32048  atomli  32068  chirredlem3  32078  sumdmdii  32101  sumdmdlem  32104  sumdmdlem2  32105