Theorem chshii 31259

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

Syntax hints:   ∈ wcel 2108   S_ℋ csh 30960   C_ℋ cch 30961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fv 6581  df-ov 7451  df-ch 31253

This theorem is referenced by:  chssii  31263  helsh  31277  h0elsh  31288  hhsscms  31310  hhssbnOLD  31311  chocunii  31333  shsleji  31402  shjshcli  31408  pjhthlem1  31423  pjhthlem2  31424  omlsii  31435  ococi  31437  pjoc1i  31463  chne0i  31485  chocini  31486  chjcli  31489  chsleji  31490  chseli  31491  chunssji  31499  chjcomi  31500  chub1i  31501  chlubi  31503  chlej1i  31505  chlej2i  31506  h1de2bi  31586  h1de2ctlem  31587  spansnpji  31610  spanunsni  31611  h1datomi  31613  pjoml2i  31617  qlaxr3i  31668  osumi  31674  osumcor2i  31676  spansnji  31678  spansnm0i  31682  nonbooli  31683  spansncvi  31684  5oai  31693  3oalem2  31695  3oalem5  31698  3oalem6  31699  pjaddii  31707  pjmulii  31709  pjss2i  31712  pjssmii  31713  pj0i  31725  pjocini  31730  pjjsi  31732  pjpythi  31754  mayete3i  31760  pjnmopi  32180  pjimai  32208  pjclem4  32231  pj3si  32239  sto1i  32268  stlei  32272  strlem1  32282  hatomici  32391  hatomistici  32394  atomli  32414  chirredlem3  32424  sumdmdii  32447  sumdmdlem  32450  sumdmdlem2  32451