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\in {CPreHil}_{\mathrm{OLD}}$$
Assertion	phnvi	$$⊢U\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		phnvi.1	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
2		phnv	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$
3	1 2	ax-mp	$$⊢U\in \mathrm{NrmCVec}$$