Theorem chshii 31228

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

Syntax hints:   ∈ wcel 2113   S_ℋ csh 30929   C_ℋ cch 30930

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fv 6497  df-ov 7358  df-ch 31222

This theorem is referenced by:  chssii  31232  helsh  31246  h0elsh  31257  hhsscms  31279  hhssbnOLD  31280  chocunii  31302  shsleji  31371  shjshcli  31377  pjhthlem1  31392  pjhthlem2  31393  omlsii  31404  ococi  31406  pjoc1i  31432  chne0i  31454  chocini  31455  chjcli  31458  chsleji  31459  chseli  31460  chunssji  31468  chjcomi  31469  chub1i  31470  chlubi  31472  chlej1i  31474  chlej2i  31475  h1de2bi  31555  h1de2ctlem  31556  spansnpji  31579  spanunsni  31580  h1datomi  31582  pjoml2i  31586  qlaxr3i  31637  osumi  31643  osumcor2i  31645  spansnji  31647  spansnm0i  31651  nonbooli  31652  spansncvi  31653  5oai  31662  3oalem2  31664  3oalem5  31667  3oalem6  31668  pjaddii  31676  pjmulii  31678  pjss2i  31681  pjssmii  31682  pj0i  31694  pjocini  31699  pjjsi  31701  pjpythi  31723  mayete3i  31729  pjnmopi  32149  pjimai  32177  pjclem4  32200  pj3si  32208  sto1i  32237  stlei  32241  strlem1  32251  hatomici  32360  hatomistici  32363  atomli  32383  chirredlem3  32393  sumdmdii  32416  sumdmdlem  32419  sumdmdlem2  32420