Theorem phnvi 31239

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

This proof depends on syntax axioms:   ∈ wcel 2146  NrmCVeccnv 31007  CPreHil_OLDccphlo 31235

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923  df-ph 31236

This theorem is used by:  elimph  31243  ip0i  31248  ip1ilem  31249  ip2i  31251  ipdirilem  31252  ipasslem1  31254  ipasslem2  31255  ipasslem4  31257  ipasslem5  31258  ipasslem7  31259  ipasslem8  31260  ipasslem9  31261  ipasslem10  31262  ipasslem11  31263  ip2dii  31267  pythi  31273  siilem1  31274  siilem2  31275  siii  31276  ipblnfi  31278  ip2eqi  31279  ajfuni  31282