Theorem phnvi 27055

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

Syntax hints:   ∈ wcel 1977  NrmCVeccnv 26823  CPreHil_OLDccphlo 27051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-ph 27052

This theorem is referenced by:  elimph  27059  ip0i  27064  ip1ilem  27065  ip2i  27067  ipdirilem  27068  ipasslem1  27070  ipasslem2  27071  ipasslem4  27073  ipasslem5  27074  ipasslem7  27075  ipasslem8  27076  ipasslem9  27077  ipasslem10  27078  ipasslem11  27079  ip2dii  27083  pythi  27089  siilem1  27090  siilem2  27091  siii  27092  ipblnfi  27095  ip2eqi  27096  ajfuni  27099