Theorem phnvi 31108

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

Syntax hints:   ∈ wcel 2149  NrmCVeccnv 30876  CPreHil_OLDccphlo 31104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930  df-ph 31105

This theorem is referenced by:  elimph  31112  ip0i  31117  ip1ilem  31118  ip2i  31120  ipdirilem  31121  ipasslem1  31123  ipasslem2  31124  ipasslem4  31126  ipasslem5  31127  ipasslem7  31128  ipasslem8  31129  ipasslem9  31130  ipasslem10  31131  ipasslem11  31132  ip2dii  31136  pythi  31142  siilem1  31143  siilem2  31144  siii  31145  ipblnfi  31147  ip2eqi  31148  ajfuni  31151