Theorem chshi 9092

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 9091	. 2 |- (H e. CH -> H e. SH)
3	1, 2	ax-mp 7	1 |- H e. SH

Syntax hints:   e. wcel 960  SHcsh 8792  CHcch 8793

This theorem is referenced by:  chssi 9096  helsh 9112  h0elsh 9123  hhsscms 9145  hhssbn 9146  hhsshl 9147  chocuni 9167  projlem18 9198  projlemHIL 9213  pjthlem12 9225  pjthlem14 9227  omlsi 9240  ococ 9242  pjoc1 9259  shjshcl 9340  chne0 9371  chocin 9372  chjcl 9375  chslej 9376  chsel 9377  chunssj 9385  chjcom 9386  chub1 9387  chlub 9389  chlej1 9391  chlej2 9392  h1de2b 9472  h1de2ctlem 9473  spansnpj 9496  spanunsn 9497  h1datom 9499  pjoml2 9523  qlaxr3 9572  osumlem2 9574  osumlem4 9576  osumlem5 9577  osumlem7 9579  osum 9581  osumcor2 9585  spansnj 9586  spansnm0 9590  nonbool 9591  spansncv 9592  5oa 9601  3oalem2 9603  3oalem5 9606  3oalem6 9607  pjadd 9615  pjmul 9617  pjss2 9620  pjssm 9621  pj0 9633  pjocin 9638  pjjs 9640  pjpyth 9662  mayete3 9668  pjnmop 10070  pjima 10099  pjclem4 10122  pj3s 10130  sto1 10158  stle 10162  strlem1 10172  hatomic 10281  hatomistic 10284  atoml 10304  irredlem3 10314  sumdmdi 10337  sumdmdlem 10340  sumdmdlem2 10341

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056  df-ch 9087

Copyright terms: Public domain