Theorem chshii 31316

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

Syntax hints:   ∈ wcel 2119   S_ℋ csh 31017   C_ℋ cch 31018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fv 6493  df-ov 7359  df-ch 31310

This theorem is referenced by:  chssii  31320  helsh  31334  h0elsh  31345  hhsscms  31367  hhssbnOLD  31368  chocunii  31390  shsleji  31459  shjshcli  31465  pjhthlem1  31480  pjhthlem2  31481  omlsii  31492  ococi  31494  pjoc1i  31520  chne0i  31542  chocini  31543  chjcli  31546  chsleji  31547  chseli  31548  chunssji  31556  chjcomi  31557  chub1i  31558  chlubi  31560  chlej1i  31562  chlej2i  31563  h1de2bi  31643  h1de2ctlem  31644  spansnpji  31667  spanunsni  31668  h1datomi  31670  pjoml2i  31674  qlaxr3i  31725  osumi  31731  osumcor2i  31733  spansnji  31735  spansnm0i  31739  nonbooli  31740  spansncvi  31741  5oai  31750  3oalem2  31752  3oalem5  31755  3oalem6  31756  pjaddii  31764  pjmulii  31766  pjss2i  31769  pjssmii  31770  pj0i  31782  pjocini  31787  pjjsi  31789  pjpythi  31811  mayete3i  31817  pjnmopi  32237  pjimai  32265  pjclem4  32288  pj3si  32296  sto1i  32325  stlei  32329  strlem1  32339  hatomici  32448  hatomistici  32451  atomli  32471  chirredlem3  32481  sumdmdii  32504  sumdmdlem  32507  sumdmdlem2  32508