Theorem chshii 27468

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

Syntax hints:   ∈ wcel 1977   S_ℋ csh 27169   C_ℋ cch 27170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fv 5812  df-ov 6552  df-ch 27462

This theorem is referenced by:  chssii  27472  helsh  27486  h0elsh  27497  hhsscms  27520  hhssbn  27521  hhsshl  27522  chocunii  27544  shsleji  27613  shjshcli  27619  pjhthlem1  27634  pjhthlem2  27635  omlsii  27646  ococi  27648  pjoc1i  27674  chne0i  27696  chocini  27697  chjcli  27700  chsleji  27701  chseli  27702  chunssji  27710  chjcomi  27711  chub1i  27712  chlubi  27714  chlej1i  27716  chlej2i  27717  h1de2bi  27797  h1de2ctlem  27798  spansnpji  27821  spanunsni  27822  h1datomi  27824  pjoml2i  27828  qlaxr3i  27879  osumi  27885  osumcor2i  27887  spansnji  27889  spansnm0i  27893  nonbooli  27894  spansncvi  27895  5oai  27904  3oalem2  27906  3oalem5  27909  3oalem6  27910  pjaddii  27918  pjmulii  27920  pjss2i  27923  pjssmii  27924  pj0i  27936  pjocini  27941  pjjsi  27943  pjpythi  27965  mayete3i  27971  pjnmopi  28391  pjimai  28419  pjclem4  28442  pj3si  28450  sto1i  28479  stlei  28483  strlem1  28493  hatomici  28602  hatomistici  28605  atomli  28625  chirredlem3  28635  sumdmdii  28658  sumdmdlem  28661  sumdmdlem2  28662