Theorem necon1d

Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008) (Proof shortened by Andrew Salmon, 25-May-2011)

	Ref	Expression
Hypothesis	necon1d.1	$$⊢\phi \to \left(A\ne B\to C=D\right)$$
Assertion	necon1d	$$⊢\phi \to \left(C\ne D\to A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		necon1d.1	$$⊢\phi \to \left(A\ne B\to C=D\right)$$
2		nne	$$⊢\neg C\ne D\leftrightarrow C=D$$
3	1 2	imbitrrdi	$$⊢\phi \to \left(A\ne B\to \neg C\ne D\right)$$
4	3	necon4ad	$$⊢\phi \to \left(C\ne D\to A=B\right)$$