This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 + : ×

Detailed syntax breakdown

Step Hyp Ref Expression
0 cva class +
1 chba class
2 1 1 cxp class ×
3 2 1 0 wf wff + : ×