Theorem chshii 31708

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

This proof depends on syntax axioms:   ∈ wcel 2145   S_ℋ csh 31409   C_ℋ cch 31410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fv 6541  df-ov 7416  df-ch 31702

This theorem is used by:  chssii  31712  helsh  31726  h0elsh  31737  hhsscms  31759  hhssbnOLD  31760  chocunii  31782  shsleji  31851  shjshcli  31857  pjhthlem1  31872  pjhthlem2  31873  omlsii  31884  ococi  31886  pjoc1i  31912  chne0i  31934  chocini  31935  chjcli  31938  chsleji  31939  chseli  31940  chunssji  31948  chjcomi  31949  chub1i  31950  chlubi  31952  chlej1i  31954  chlej2i  31955  h1de2bi  32035  h1de2ctlem  32036  spansnpji  32059  spanunsni  32060  h1datomi  32062  pjoml2i  32066  qlaxr3i  32117  osumi  32123  osumcor2i  32125  spansnji  32127  spansnm0i  32131  nonbooli  32132  spansncvi  32133  5oai  32142  3oalem2  32144  3oalem5  32147  3oalem6  32148  pjaddii  32156  pjmulii  32158  pjss2i  32161  pjssmii  32162  pj0i  32174  pjocini  32179  pjjsi  32181  pjpythi  32203  mayete3i  32209  pjnmopi  32629  pjimai  32657  pjclem4  32680  pj3si  32688  sto1i  32717  stlei  32721  strlem1  32731  hatomici  32840  hatomistici  32843  atomli  32863  chirredlem3  32873  sumdmdii  32896  sumdmdlem  32899  sumdmdlem2  32900