Theorem phnvi 31411

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

This proof depends on syntax axioms:   ∈ wcel 2145  NrmCVeccnv 31179  CPreHil_OLDccphlo 31407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-ph 31408

This theorem is used by:  elimph  31415  ip0i  31420  ip1ilem  31421  ip2i  31423  ipdirilem  31424  ipasslem1  31426  ipasslem2  31427  ipasslem4  31429  ipasslem5  31430  ipasslem7  31431  ipasslem8  31432  ipasslem9  31433  ipasslem10  31434  ipasslem11  31435  ip2dii  31439  pythi  31445  siilem1  31446  siilem2  31447  siii  31448  ipblnfi  31450  ip2eqi  31451  ajfuni  31454