Theorem phnvi 29227

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

Syntax hints:   ∈ wcel 2104  NrmCVeccnv 28995  CPreHil_OLDccphlo 29223

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-ph 29224

This theorem is referenced by:  elimph  29231  ip0i  29236  ip1ilem  29237  ip2i  29239  ipdirilem  29240  ipasslem1  29242  ipasslem2  29243  ipasslem4  29245  ipasslem5  29246  ipasslem7  29247  ipasslem8  29248  ipasslem9  29249  ipasslem10  29250  ipasslem11  29251  ip2dii  29255  pythi  29261  siilem1  29262  siilem2  29263  siii  29264  ipblnfi  29266  ip2eqi  29267  ajfuni  29270