Theorem phnvi 30905

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

Syntax hints:   ∈ wcel 2119  NrmCVeccnv 30673  CPreHil_OLDccphlo 30901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900  df-ph 30902

This theorem is referenced by:  elimph  30909  ip0i  30914  ip1ilem  30915  ip2i  30917  ipdirilem  30918  ipasslem1  30920  ipasslem2  30921  ipasslem4  30923  ipasslem5  30924  ipasslem7  30925  ipasslem8  30926  ipasslem9  30927  ipasslem10  30928  ipasslem11  30929  ip2dii  30933  pythi  30939  siilem1  30940  siilem2  30941  siii  30942  ipblnfi  30944  ip2eqi  30945  ajfuni  30948