Theorem phnvi 30324

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 30322	. 2 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)
3	1, 2	ax-mp 5	1 ⊢ 𝑈 ∈ NrmCVec

Syntax hints:   ∈ wcel 2106  NrmCVeccnv 30092  CPreHil_OLDccphlo 30320

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-ph 30321

This theorem is referenced by:  elimph  30328  ip0i  30333  ip1ilem  30334  ip2i  30336  ipdirilem  30337  ipasslem1  30339  ipasslem2  30340  ipasslem4  30342  ipasslem5  30343  ipasslem7  30344  ipasslem8  30345  ipasslem9  30346  ipasslem10  30347  ipasslem11  30348  ip2dii  30352  pythi  30358  siilem1  30359  siilem2  30360  siii  30361  ipblnfi  30363  ip2eqi  30364  ajfuni  30367