This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to (A \neq B \to C = D)$
	Assertion	necon1d	$⊢ φ \to (C \neq D \to A = B)$

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