Theorem chshii 29589

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

Syntax hints:   ∈ wcel 2106   S_ℋ csh 29290   C_ℋ cch 29291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fv 6441  df-ov 7278  df-ch 29583

This theorem is referenced by:  chssii  29593  helsh  29607  h0elsh  29618  hhsscms  29640  hhssbnOLD  29641  chocunii  29663  shsleji  29732  shjshcli  29738  pjhthlem1  29753  pjhthlem2  29754  omlsii  29765  ococi  29767  pjoc1i  29793  chne0i  29815  chocini  29816  chjcli  29819  chsleji  29820  chseli  29821  chunssji  29829  chjcomi  29830  chub1i  29831  chlubi  29833  chlej1i  29835  chlej2i  29836  h1de2bi  29916  h1de2ctlem  29917  spansnpji  29940  spanunsni  29941  h1datomi  29943  pjoml2i  29947  qlaxr3i  29998  osumi  30004  osumcor2i  30006  spansnji  30008  spansnm0i  30012  nonbooli  30013  spansncvi  30014  5oai  30023  3oalem2  30025  3oalem5  30028  3oalem6  30029  pjaddii  30037  pjmulii  30039  pjss2i  30042  pjssmii  30043  pj0i  30055  pjocini  30060  pjjsi  30062  pjpythi  30084  mayete3i  30090  pjnmopi  30510  pjimai  30538  pjclem4  30561  pj3si  30569  sto1i  30598  stlei  30602  strlem1  30612  hatomici  30721  hatomistici  30724  atomli  30744  chirredlem3  30754  sumdmdii  30777  sumdmdlem  30780  sumdmdlem2  30781