Theorem chshii 31129

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

Syntax hints:   ∈ wcel 2109   S_ℋ csh 30830   C_ℋ cch 30831

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fv 6507  df-ov 7372  df-ch 31123

This theorem is referenced by:  chssii  31133  helsh  31147  h0elsh  31158  hhsscms  31180  hhssbnOLD  31181  chocunii  31203  shsleji  31272  shjshcli  31278  pjhthlem1  31293  pjhthlem2  31294  omlsii  31305  ococi  31307  pjoc1i  31333  chne0i  31355  chocini  31356  chjcli  31359  chsleji  31360  chseli  31361  chunssji  31369  chjcomi  31370  chub1i  31371  chlubi  31373  chlej1i  31375  chlej2i  31376  h1de2bi  31456  h1de2ctlem  31457  spansnpji  31480  spanunsni  31481  h1datomi  31483  pjoml2i  31487  qlaxr3i  31538  osumi  31544  osumcor2i  31546  spansnji  31548  spansnm0i  31552  nonbooli  31553  spansncvi  31554  5oai  31563  3oalem2  31565  3oalem5  31568  3oalem6  31569  pjaddii  31577  pjmulii  31579  pjss2i  31582  pjssmii  31583  pj0i  31595  pjocini  31600  pjjsi  31602  pjpythi  31624  mayete3i  31630  pjnmopi  32050  pjimai  32078  pjclem4  32101  pj3si  32109  sto1i  32138  stlei  32142  strlem1  32152  hatomici  32261  hatomistici  32264  atomli  32284  chirredlem3  32294  sumdmdii  32317  sumdmdlem  32320  sumdmdlem2  32321