Theorem phnvi 29157

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

Syntax hints:   ∈ wcel 2109  NrmCVeccnv 28925  CPreHil_OLDccphlo 29153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-ph 29154

This theorem is referenced by:  elimph  29161  ip0i  29166  ip1ilem  29167  ip2i  29169  ipdirilem  29170  ipasslem1  29172  ipasslem2  29173  ipasslem4  29175  ipasslem5  29176  ipasslem7  29177  ipasslem8  29178  ipasslem9  29179  ipasslem10  29180  ipasslem11  29181  ip2dii  29185  pythi  29191  siilem1  29192  siilem2  29193  siii  29194  ipblnfi  29196  ip2eqi  29197  ajfuni  29200