Theorem phnvi 30760

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

Syntax hints:   ∈ wcel 2109  NrmCVeccnv 30528  CPreHil_OLDccphlo 30756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910  df-ss 3920  df-ph 30757

This theorem is referenced by:  elimph  30764  ip0i  30769  ip1ilem  30770  ip2i  30772  ipdirilem  30773  ipasslem1  30775  ipasslem2  30776  ipasslem4  30778  ipasslem5  30779  ipasslem7  30780  ipasslem8  30781  ipasslem9  30782  ipasslem10  30783  ipasslem11  30784  ip2dii  30788  pythi  30794  siilem1  30795  siilem2  30796  siii  30797  ipblnfi  30799  ip2eqi  30800  ajfuni  30803