Theorem phnvi 31297

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

This proof depends on syntax axioms:   ∈ wcel 2145  NrmCVeccnv 31065  CPreHil_OLDccphlo 31293

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916  df-ph 31294

This theorem is used by:  elimph  31301  ip0i  31306  ip1ilem  31307  ip2i  31309  ipdirilem  31310  ipasslem1  31312  ipasslem2  31313  ipasslem4  31315  ipasslem5  31316  ipasslem7  31317  ipasslem8  31318  ipasslem9  31319  ipasslem10  31320  ipasslem11  31321  ip2dii  31325  pythi  31331  siilem1  31332  siilem2  31333  siii  31334  ipblnfi  31336  ip2eqi  31337  ajfuni  31340