Theorem negned

Description: If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	negidd.1	|- ( ph -> A e. CC )
	negned.2	|- ( ph -> B e. CC )
	negned.3	|- ( ph -> A =/= B )
Assertion	negned	|- ( ph -> -u A =/= -u B )

Proof

Step	Hyp	Ref	Expression
1		negidd.1	|- ( ph -> A e. CC )
2		negned.2	|- ( ph -> B e. CC )
3		negned.3	|- ( ph -> A =/= B )
4	1 2	neg11ad	|- ( ph -> ( -u A = -u B <-> A = B ) )
5	4	necon3bid	|- ( ph -> ( -u A =/= -u B <-> A =/= B ) )
6	3 5	mpbird	|- ( ph -> -u A =/= -u B )