Theorem phnvi 30796

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

Syntax hints:   ∈ wcel 2111  NrmCVeccnv 30564  CPreHil_OLDccphlo 30792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-ss 3914  df-ph 30793

This theorem is referenced by:  elimph  30800  ip0i  30805  ip1ilem  30806  ip2i  30808  ipdirilem  30809  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem5  30815  ipasslem7  30816  ipasslem8  30817  ipasslem9  30818  ipasslem10  30819  ipasslem11  30820  ip2dii  30824  pythi  30830  siilem1  30831  siilem2  30832  siii  30833  ipblnfi  30835  ip2eqi  30836  ajfuni  30839