Theorem chshii 28084

Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
chshi.1	|- H e. CH

Assertion

Ref	Expression
chshii	|- H e. SH

Proof of Theorem chshii

Step	Hyp	Ref	Expression
1		chshi.1	. 2 |- H e. CH
2		chsh 28081	. 2 |- ( H e. CH -> H e. SH )
3	1, 2	ax-mp 5	1 |- H e. SH

Syntax hints:   e. wcel 1990   SHcsh 27785   CHcch 27786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fv 5896  df-ov 6653  df-ch 28078

This theorem is referenced by:  chssii  28088  helsh  28102  h0elsh  28113  hhsscms  28136  hhssbn  28137  hhsshl  28138  chocunii  28160  shsleji  28229  shjshcli  28235  pjhthlem1  28250  pjhthlem2  28251  omlsii  28262  ococi  28264  pjoc1i  28290  chne0i  28312  chocini  28313  chjcli  28316  chsleji  28317  chseli  28318  chunssji  28326  chjcomi  28327  chub1i  28328  chlubi  28330  chlej1i  28332  chlej2i  28333  h1de2bi  28413  h1de2ctlem  28414  spansnpji  28437  spanunsni  28438  h1datomi  28440  pjoml2i  28444  qlaxr3i  28495  osumi  28501  osumcor2i  28503  spansnji  28505  spansnm0i  28509  nonbooli  28510  spansncvi  28511  5oai  28520  3oalem2  28522  3oalem5  28525  3oalem6  28526  pjaddii  28534  pjmulii  28536  pjss2i  28539  pjssmii  28540  pj0i  28552  pjocini  28557  pjjsi  28559  pjpythi  28581  mayete3i  28587  pjnmopi  29007  pjimai  29035  pjclem4  29058  pj3si  29066  sto1i  29095  stlei  29099  strlem1  29109  hatomici  29218  hatomistici  29221  atomli  29241  chirredlem3  29251  sumdmdii  29274  sumdmdlem  29277  sumdmdlem2  29278