Theorem phnvi 28599

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

Hypothesis

Ref	Expression
phnvi.1	⊢ 𝑈 ∈ CPreHilOLD

Assertion

Ref	Expression
phnvi	⊢ 𝑈 ∈ NrmCVec

Proof of Theorem phnvi

Step	Hyp	Ref	Expression
1		phnvi.1	. 2 ⊢ 𝑈 ∈ CPreHilOLD
2		phnv 28597	. 2 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)
3	1, 2	ax-mp 5	1 ⊢ 𝑈 ∈ NrmCVec

Syntax hints:   ∈ wcel 2111  NrmCVeccnv 28367  CPreHil_OLDccphlo 28595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-ph 28596

This theorem is referenced by:  elimph  28603  ip0i  28608  ip1ilem  28609  ip2i  28611  ipdirilem  28612  ipasslem1  28614  ipasslem2  28615  ipasslem4  28617  ipasslem5  28618  ipasslem7  28619  ipasslem8  28620  ipasslem9  28621  ipasslem10  28622  ipasslem11  28623  ip2dii  28627  pythi  28633  siilem1  28634  siilem2  28635  siii  28636  ipblnfi  28638  ip2eqi  28639  ajfuni  28642