Theorem hvaddlidi

Description: Addition with the zero vector. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hvaddlid.1	|- A e. ~H
Assertion	hvaddlidi	|- ( 0h +h A ) = A

Proof

Step	Hyp	Ref	Expression
1		hvaddlid.1	|- A e. ~H
2		hvaddlid	|- ( A e. ~H -> ( 0h +h A ) = A )
3	1 2	ax-mp	|- ( 0h +h A ) = A