Theorem phnvi 30797

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

Syntax hints:   ∈ wcel 2108  NrmCVeccnv 30565  CPreHil_OLDccphlo 30793

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943  df-ph 30794

This theorem is referenced by:  elimph  30801  ip0i  30806  ip1ilem  30807  ip2i  30809  ipdirilem  30810  ipasslem1  30812  ipasslem2  30813  ipasslem4  30815  ipasslem5  30816  ipasslem7  30817  ipasslem8  30818  ipasslem9  30819  ipasslem10  30820  ipasslem11  30821  ip2dii  30825  pythi  30831  siilem1  30832  siilem2  30833  siii  30834  ipblnfi  30836  ip2eqi  30837  ajfuni  30840