Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  phnvi Structured version   Unicode version

Theorem phnvi 22309
 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
Assertion
Ref Expression
phnvi

Proof of Theorem phnvi
StepHypRef Expression
1 phnvi.1 . 2
2 phnv 22307 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wcel 1725  cnv 22055  ccphlo 22305 This theorem is referenced by:  elimph  22313  ip0i  22318  ip1ilem  22319  ip2i  22321  ipdirilem  22322  ipasslem1  22324  ipasslem2  22325  ipasslem4  22327  ipasslem5  22328  ipasslem7  22329  ipasslem8  22330  ipasslem9  22331  ipasslem10  22332  ipasslem11  22333  ip2dii  22337  pythi  22343  siilem1  22344  siilem2  22345  siii  22346  ipblnfi  22349  ip2eqi  22350  ajfuni  22353 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-ph 22306
 Copyright terms: Public domain W3C validator