Theorem chshii 31189

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

Syntax hints:   ∈ wcel 2109   S_ℋ csh 30890   C_ℋ cch 30891

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fv 6494  df-ov 7356  df-ch 31183

This theorem is referenced by:  chssii  31193  helsh  31207  h0elsh  31218  hhsscms  31240  hhssbnOLD  31241  chocunii  31263  shsleji  31332  shjshcli  31338  pjhthlem1  31353  pjhthlem2  31354  omlsii  31365  ococi  31367  pjoc1i  31393  chne0i  31415  chocini  31416  chjcli  31419  chsleji  31420  chseli  31421  chunssji  31429  chjcomi  31430  chub1i  31431  chlubi  31433  chlej1i  31435  chlej2i  31436  h1de2bi  31516  h1de2ctlem  31517  spansnpji  31540  spanunsni  31541  h1datomi  31543  pjoml2i  31547  qlaxr3i  31598  osumi  31604  osumcor2i  31606  spansnji  31608  spansnm0i  31612  nonbooli  31613  spansncvi  31614  5oai  31623  3oalem2  31625  3oalem5  31628  3oalem6  31629  pjaddii  31637  pjmulii  31639  pjss2i  31642  pjssmii  31643  pj0i  31655  pjocini  31660  pjjsi  31662  pjpythi  31684  mayete3i  31690  pjnmopi  32110  pjimai  32138  pjclem4  32161  pj3si  32169  sto1i  32198  stlei  32202  strlem1  32212  hatomici  32321  hatomistici  32324  atomli  32344  chirredlem3  32354  sumdmdii  32377  sumdmdlem  32380  sumdmdlem2  32381