Metamath Proof Explorer

Axiom ax-hfvadd

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cva 
 |-  +h
1 chba 
 |-  ~H
2 1 1 cxp 
 |-  ( ~H X. ~H )
3 2 1 0 wf 
 |-  +h : ( ~H X. ~H ) --> ~H