Theorem chshii 31109

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

Syntax hints:   ∈ wcel 2098   S_ℋ csh 30810   C_ℋ cch 30811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5684  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fv 6557  df-ov 7422  df-ch 31103

This theorem is referenced by:  chssii  31113  helsh  31127  h0elsh  31138  hhsscms  31160  hhssbnOLD  31161  chocunii  31183  shsleji  31252  shjshcli  31258  pjhthlem1  31273  pjhthlem2  31274  omlsii  31285  ococi  31287  pjoc1i  31313  chne0i  31335  chocini  31336  chjcli  31339  chsleji  31340  chseli  31341  chunssji  31349  chjcomi  31350  chub1i  31351  chlubi  31353  chlej1i  31355  chlej2i  31356  h1de2bi  31436  h1de2ctlem  31437  spansnpji  31460  spanunsni  31461  h1datomi  31463  pjoml2i  31467  qlaxr3i  31518  osumi  31524  osumcor2i  31526  spansnji  31528  spansnm0i  31532  nonbooli  31533  spansncvi  31534  5oai  31543  3oalem2  31545  3oalem5  31548  3oalem6  31549  pjaddii  31557  pjmulii  31559  pjss2i  31562  pjssmii  31563  pj0i  31575  pjocini  31580  pjjsi  31582  pjpythi  31604  mayete3i  31610  pjnmopi  32030  pjimai  32058  pjclem4  32081  pj3si  32089  sto1i  32118  stlei  32122  strlem1  32132  hatomici  32241  hatomistici  32244  atomli  32264  chirredlem3  32274  sumdmdii  32297  sumdmdlem  32300  sumdmdlem2  32301