Theorem phnvi 30845

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

Syntax hints:   ∈ wcel 2106  NrmCVeccnv 30613  CPreHil_OLDccphlo 30841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ss 3980  df-ph 30842

This theorem is referenced by:  elimph  30849  ip0i  30854  ip1ilem  30855  ip2i  30857  ipdirilem  30858  ipasslem1  30860  ipasslem2  30861  ipasslem4  30863  ipasslem5  30864  ipasslem7  30865  ipasslem8  30866  ipasslem9  30867  ipasslem10  30868  ipasslem11  30869  ip2dii  30873  pythi  30879  siilem1  30880  siilem2  30881  siii  30882  ipblnfi  30884  ip2eqi  30885  ajfuni  30888