Axiom ax-hfvmul 27862

Description: Scalar multiplication is an operation on CC and ~H. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hfvmul	|- .h : ( CC X. ~H ) --> ~H

Detailed syntax breakdown of Axiom ax-hfvmul

Step	Hyp	Ref	Expression
1		cc 9934	. . 3 class CC
2		chil 27776	. . 3 class ~H
3	1, 2	cxp 5112	. 2 class ( CC X. ~H )
4		csm 27778	. 2 class .h
5	3, 2, 4	wf 5884	1 wff .h : ( CC X. ~H ) --> ~H

This axiom is referenced by:  hvmulex  27868  hvmulcl  27870  hilvc  28019  issh2  28066  hhssabloilem  28118  hhssnv  28121  hhsssh  28126