Theorem phnvi 31427

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

This proof depends on syntax axioms:   ∈ wcel 2144  NrmCVeccnv 31195  CPreHil_OLDccphlo 31423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-in 4090  df-ph 31424

This theorem is used by:  elimph  31431  ip0i  31436  ip1ilem  31437  ip2i  31439  ipdirilem  31440  ipasslem1  31442  ipasslem2  31443  ipasslem4  31445  ipasslem5  31446  ipasslem7  31447  ipasslem8  31448  ipasslem9  31449  ipasslem10  31450  ipasslem11  31451  ip2dii  31455  pythi  31461  siilem1  31462  siilem2  31463  siii  31464  ipblnfi  31466  ip2eqi  31467  ajfuni  31470