Axiom ax-hfi 22534

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

Assertion

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

Detailed syntax breakdown of Axiom ax-hfi

Step	Hyp	Ref	Expression
1		chil 22375	. . 3 class ~H
2	1, 1	cxp 4835	. 2 class ( ~H X. ~H )
3		cc 8944	. 2 class CC
4		csp 22378	. 2 class .ih
5	2, 3, 4	wf 5409	1 wff .ih : ( ~H X. ~H ) --> CC

This axiom is referenced by:  hicl  22535  dfhnorm2  22577  hhip  22632