Theorem negidd

Description: Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypothesis	negidd.1	|- ( ph -> A e. CC )
Assertion	negidd	|- ( ph -> ( A + -u A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		negidd.1	|- ( ph -> A e. CC )
2		negid	|- ( A e. CC -> ( A + -u A ) = 0 )
3	1 2	syl	|- ( ph -> ( A + -u A ) = 0 )