Theorem chshii 31302

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

Syntax hints:   ∈ wcel 2113   S_ℋ csh 31003   C_ℋ cch 31004

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fv 6500  df-ov 7361  df-ch 31296

This theorem is referenced by:  chssii  31306  helsh  31320  h0elsh  31331  hhsscms  31353  hhssbnOLD  31354  chocunii  31376  shsleji  31445  shjshcli  31451  pjhthlem1  31466  pjhthlem2  31467  omlsii  31478  ococi  31480  pjoc1i  31506  chne0i  31528  chocini  31529  chjcli  31532  chsleji  31533  chseli  31534  chunssji  31542  chjcomi  31543  chub1i  31544  chlubi  31546  chlej1i  31548  chlej2i  31549  h1de2bi  31629  h1de2ctlem  31630  spansnpji  31653  spanunsni  31654  h1datomi  31656  pjoml2i  31660  qlaxr3i  31711  osumi  31717  osumcor2i  31719  spansnji  31721  spansnm0i  31725  nonbooli  31726  spansncvi  31727  5oai  31736  3oalem2  31738  3oalem5  31741  3oalem6  31742  pjaddii  31750  pjmulii  31752  pjss2i  31755  pjssmii  31756  pj0i  31768  pjocini  31773  pjjsi  31775  pjpythi  31797  mayete3i  31803  pjnmopi  32223  pjimai  32251  pjclem4  32274  pj3si  32282  sto1i  32311  stlei  32315  strlem1  32325  hatomici  32434  hatomistici  32437  atomli  32457  chirredlem3  32467  sumdmdii  32490  sumdmdlem  32493  sumdmdlem2  32494