Theorem phnvi 30891

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

Syntax hints:   ∈ wcel 2113  NrmCVeccnv 30659  CPreHil_OLDccphlo 30887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-ph 30888

This theorem is referenced by:  elimph  30895  ip0i  30900  ip1ilem  30901  ip2i  30903  ipdirilem  30904  ipasslem1  30906  ipasslem2  30907  ipasslem4  30909  ipasslem5  30910  ipasslem7  30911  ipasslem8  30912  ipasslem9  30913  ipasslem10  30914  ipasslem11  30915  ip2dii  30919  pythi  30925  siilem1  30926  siilem2  30927  siii  30928  ipblnfi  30930  ip2eqi  30931  ajfuni  30934