Theorem phnvi 30718

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

Syntax hints:   ∈ wcel 2109  NrmCVeccnv 30486  CPreHil_OLDccphlo 30714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ss 3928  df-ph 30715

This theorem is referenced by:  elimph  30722  ip0i  30727  ip1ilem  30728  ip2i  30730  ipdirilem  30731  ipasslem1  30733  ipasslem2  30734  ipasslem4  30736  ipasslem5  30737  ipasslem7  30738  ipasslem8  30739  ipasslem9  30740  ipasslem10  30741  ipasslem11  30742  ip2dii  30746  pythi  30752  siilem1  30753  siilem2  30754  siii  30755  ipblnfi  30757  ip2eqi  30758  ajfuni  30761