Theorem chshii 31199

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

Syntax hints:   ∈ wcel 2111   S_ℋ csh 30900   C_ℋ cch 30901

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-xp 5617  df-cnv 5619  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fv 6484  df-ov 7344  df-ch 31193

This theorem is referenced by:  chssii  31203  helsh  31217  h0elsh  31228  hhsscms  31250  hhssbnOLD  31251  chocunii  31273  shsleji  31342  shjshcli  31348  pjhthlem1  31363  pjhthlem2  31364  omlsii  31375  ococi  31377  pjoc1i  31403  chne0i  31425  chocini  31426  chjcli  31429  chsleji  31430  chseli  31431  chunssji  31439  chjcomi  31440  chub1i  31441  chlubi  31443  chlej1i  31445  chlej2i  31446  h1de2bi  31526  h1de2ctlem  31527  spansnpji  31550  spanunsni  31551  h1datomi  31553  pjoml2i  31557  qlaxr3i  31608  osumi  31614  osumcor2i  31616  spansnji  31618  spansnm0i  31622  nonbooli  31623  spansncvi  31624  5oai  31633  3oalem2  31635  3oalem5  31638  3oalem6  31639  pjaddii  31647  pjmulii  31649  pjss2i  31652  pjssmii  31653  pj0i  31665  pjocini  31670  pjjsi  31672  pjpythi  31694  mayete3i  31700  pjnmopi  32120  pjimai  32148  pjclem4  32171  pj3si  32179  sto1i  32208  stlei  32212  strlem1  32222  hatomici  32331  hatomistici  32334  atomli  32354  chirredlem3  32364  sumdmdii  32387  sumdmdlem  32390  sumdmdlem2  32391