Metamath Proof Explorer

Axiom ax-hfi

Description: Inner product maps pairs from ~H to CC . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Assertion ax-hfi 
|- .ih : ( ~H X. ~H ) --> CC

Detailed syntax breakdown

Step Hyp Ref Expression
0 csp 
 |-  .ih
1 chba 
 |-  ~H
2 1 1 cxp 
 |-  ( ~H X. ~H )
3 cc 
 |-  CC
4 2 3 0 wf 
 |-  .ih : ( ~H X. ~H ) --> CC