Metamath Proof Explorer

Theorem hlobn

Description: Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hlobn 
|- ( U e. CHilOLD -> U e. CBan )

Proof

Step Hyp Ref Expression
1 ishlo 
 |-  ( U e. CHilOLD <-> ( U e. CBan /\ U e. CPreHilOLD ) )
2 1 simplbi 
 |-  ( U e. CHilOLD -> U e. CBan )