Theorem phnvi 29996

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

Syntax hints:   ∈ wcel 2106  NrmCVeccnv 29764  CPreHil_OLDccphlo 29992

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3952  df-ss 3962  df-ph 29993

This theorem is referenced by:  elimph  30000  ip0i  30005  ip1ilem  30006  ip2i  30008  ipdirilem  30009  ipasslem1  30011  ipasslem2  30012  ipasslem4  30014  ipasslem5  30015  ipasslem7  30016  ipasslem8  30017  ipasslem9  30018  ipasslem10  30019  ipasslem11  30020  ip2dii  30024  pythi  30030  siilem1  30031  siilem2  30032  siii  30033  ipblnfi  30035  ip2eqi  30036  ajfuni  30039