Theorem phnvi

Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	phnvi.1	|- U e. CPreHilOLD
Assertion	phnvi	|- U e. NrmCVec

Proof

Step	Hyp	Ref	Expression
1		phnvi.1	|- U e. CPreHilOLD
2		phnv	|- ( U e. CPreHilOLD -> U e. NrmCVec )
3	1 2	ax-mp	|- U e. NrmCVec