This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chsh

Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion chsh ⊢ H ∈ C ℋ → H ∈ S ℋ

Proof

Step Hyp Ref Expression
1 isch ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ⇝v H ℕ ⊆ H
2 1 simplbi ⊢ H ∈ C ℋ → H ∈ S ℋ