Theorem phnvi 30904

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

Syntax hints:   ∈ wcel 2114  NrmCVeccnv 30672  CPreHil_OLDccphlo 30900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920  df-ph 30901

This theorem is referenced by:  elimph  30908  ip0i  30913  ip1ilem  30914  ip2i  30916  ipdirilem  30917  ipasslem1  30919  ipasslem2  30920  ipasslem4  30922  ipasslem5  30923  ipasslem7  30924  ipasslem8  30925  ipasslem9  30926  ipasslem10  30927  ipasslem11  30928  ip2dii  30932  pythi  30938  siilem1  30939  siilem2  30940  siii  30941  ipblnfi  30943  ip2eqi  30944  ajfuni  30947