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

Metamath Proof Explorer

Theorem necon4d

Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

		Ref	Expression
	Hypothesis	necon4d.1	$⊢ φ \to (A \neq B \to C \neq D)$
	Assertion	necon4d	$⊢ φ \to (C = D \to A = B)$

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