Theorem phnvi 30905

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

Syntax hints:   ∈ wcel 2114  NrmCVeccnv 30673  CPreHil_OLDccphlo 30901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907  df-ph 30902

This theorem is referenced by:  elimph  30909  ip0i  30914  ip1ilem  30915  ip2i  30917  ipdirilem  30918  ipasslem1  30920  ipasslem2  30921  ipasslem4  30923  ipasslem5  30924  ipasslem7  30925  ipasslem8  30926  ipasslem9  30927  ipasslem10  30928  ipasslem11  30929  ip2dii  30933  pythi  30939  siilem1  30940  siilem2  30941  siii  30942  ipblnfi  30944  ip2eqi  30945  ajfuni  30948