Theorem hvaddlidi

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

	Ref	Expression
Hypothesis	hvaddlid.1	$$⊢A\in \mathscr{H}$$
Assertion	hvaddlidi	$$⊢0_{ℎ}{+}_{ℎ}A=A$$

Proof

Step	Hyp	Ref	Expression
1		hvaddlid.1	$$⊢A\in \mathscr{H}$$
2		hvaddlid	$$⊢A\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}A=A$$
3	1 2	ax-mp	$$⊢0_{ℎ}{+}_{ℎ}A=A$$