Theorem mulm1i

Description: Product with minus one is negative. (Contributed by NM, 31-Jul-1999)

	Ref	Expression
Hypothesis	mulm1.1	$$⊢A\in ℂ$$
Assertion	mulm1i	$$⊢-1A=-A$$

Proof

Step	Hyp	Ref	Expression
1		mulm1.1	$$⊢A\in ℂ$$
2		mulm1	$$⊢A\in ℂ\to -1A=-A$$
3	1 2	ax-mp	$$⊢-1A=-A$$