Axiom ax-hfvadd 27857

Description: Vector addition is an operation on ~H. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hfvadd	|- +h : ( ~H X. ~H ) --> ~H

Detailed syntax breakdown of Axiom ax-hfvadd

Step	Hyp	Ref	Expression
1		chil 27776	. . 3 class ~H
2	1, 1	cxp 5112	. 2 class ( ~H X. ~H )
3		cva 27777	. 2 class +h
4	2, 1, 3	wf 5884	1 wff +h : ( ~H X. ~H ) --> ~H

This axiom is referenced by:  hvaddcl  27869  hilablo  28017  hilid  28018  hilvc  28019  hhnv  28022  hhba  28024  hhph  28035  issh2  28066  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  hhsssh  28126  shsss  28172  shsel  28173