Theorem phnvi 30840

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

Syntax hints:   ∈ wcel 2113  NrmCVeccnv 30608  CPreHil_OLDccphlo 30836

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ss 3916  df-ph 30837

This theorem is referenced by:  elimph  30844  ip0i  30849  ip1ilem  30850  ip2i  30852  ipdirilem  30853  ipasslem1  30855  ipasslem2  30856  ipasslem4  30858  ipasslem5  30859  ipasslem7  30860  ipasslem8  30861  ipasslem9  30862  ipasslem10  30863  ipasslem11  30864  ip2dii  30868  pythi  30874  siilem1  30875  siilem2  30876  siii  30877  ipblnfi  30879  ip2eqi  30880  ajfuni  30883