Theorem chshi 9097

Description: A closed subspace is a subspace.

Hypothesis

Ref	Expression
chshi.1	|- H e. CH

Assertion

Ref	Expression
chshi	|- H e. SH

Proof of Theorem chshi

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

Syntax hints:   e. wcel 958  SHcsh 8797  CHcch 8798

This theorem is referenced by:  chssi 9101  helsh 9117  h0elsh 9128  hhsscms 9150  hhssbn 9151  hhsshl 9152  chocuni 9172  projlem18 9203  projlemHIL 9218  pjthlem12 9230  pjthlem14 9232  omlsi 9245  ococ 9247  pjoc1 9264  shjshcl 9345  chne0 9376  chocin 9377  chjcl 9380  chslej 9381  chsel 9382  chunssj 9390  chjcom 9391  chub1 9392  chlub 9394  chlej1 9396  chlej2 9397  h1de2b 9477  h1de2ctlem 9478  spansnpj 9501  spanunsn 9502  h1datom 9504  pjoml2 9528  qlaxr3 9577  osumlem2 9579  osumlem4 9581  osumlem5 9582  osumlem7 9584  osum 9586  osumcor2 9590  spansnj 9591  spansnm0 9595  nonbool 9596  spansncv 9597  5oa 9606  3oalem2 9608  3oalem5 9611  3oalem6 9612  pjadd 9620  pjmul 9622  pjss2 9625  pjssm 9626  pj0 9638  pjocin 9643  pjjs 9645  pjpyth 9667  mayete3 9673  pjnmop 10075  pjima 10104  pjclem4 10127  pj3s 10135  sto1 10163  stle 10167  strlem1 10177  hatomic 10286  hatomistic 10289  atoml 10309  irredlem3 10319  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-ch 9092

Copyright terms: Public domain