Theorem necon2i

Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007)

	Ref	Expression
Hypothesis	necon2i.1	|- ( A = B -> C =/= D )
Assertion	necon2i	|- ( C = D -> A =/= B )

Proof

Step	Hyp	Ref	Expression
1		necon2i.1	|- ( A = B -> C =/= D )
2	1	neneqd	|- ( A = B -> -. C = D )
3	2	necon2ai	|- ( C = D -> A =/= B )