Theorem phnvi 30887

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

Syntax hints:   ∈ wcel 2114  NrmCVeccnv 30655  CPreHil_OLDccphlo 30883

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906  df-ph 30884

This theorem is referenced by:  elimph  30891  ip0i  30896  ip1ilem  30897  ip2i  30899  ipdirilem  30900  ipasslem1  30902  ipasslem2  30903  ipasslem4  30905  ipasslem5  30906  ipasslem7  30907  ipasslem8  30908  ipasslem9  30909  ipasslem10  30910  ipasslem11  30911  ip2dii  30915  pythi  30921  siilem1  30922  siilem2  30923  siii  30924  ipblnfi  30926  ip2eqi  30927  ajfuni  30930