Theorem phnvi 31168

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

Syntax hints:   ∈ wcel 2143  NrmCVeccnv 30936  CPreHil_OLDccphlo 31164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922  df-ph 31165

This theorem is referenced by:  elimph  31172  ip0i  31177  ip1ilem  31178  ip2i  31180  ipdirilem  31181  ipasslem1  31183  ipasslem2  31184  ipasslem4  31186  ipasslem5  31187  ipasslem7  31188  ipasslem8  31189  ipasslem9  31190  ipasslem10  31191  ipasslem11  31192  ip2dii  31196  pythi  31202  siilem1  31203  siilem2  31204  siii  31205  ipblnfi  31207  ip2eqi  31208  ajfuni  31211