Theorem chshii 31256

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

Syntax hints:   ∈ wcel 2106   S_ℋ csh 30957   C_ℋ cch 30958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fv 6571  df-ov 7434  df-ch 31250

This theorem is referenced by:  chssii  31260  helsh  31274  h0elsh  31285  hhsscms  31307  hhssbnOLD  31308  chocunii  31330  shsleji  31399  shjshcli  31405  pjhthlem1  31420  pjhthlem2  31421  omlsii  31432  ococi  31434  pjoc1i  31460  chne0i  31482  chocini  31483  chjcli  31486  chsleji  31487  chseli  31488  chunssji  31496  chjcomi  31497  chub1i  31498  chlubi  31500  chlej1i  31502  chlej2i  31503  h1de2bi  31583  h1de2ctlem  31584  spansnpji  31607  spanunsni  31608  h1datomi  31610  pjoml2i  31614  qlaxr3i  31665  osumi  31671  osumcor2i  31673  spansnji  31675  spansnm0i  31679  nonbooli  31680  spansncvi  31681  5oai  31690  3oalem2  31692  3oalem5  31695  3oalem6  31696  pjaddii  31704  pjmulii  31706  pjss2i  31709  pjssmii  31710  pj0i  31722  pjocini  31727  pjjsi  31729  pjpythi  31751  mayete3i  31757  pjnmopi  32177  pjimai  32205  pjclem4  32228  pj3si  32236  sto1i  32265  stlei  32269  strlem1  32279  hatomici  32388  hatomistici  32391  atomli  32411  chirredlem3  32421  sumdmdii  32444  sumdmdlem  32447  sumdmdlem2  32448