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

Metamath Proof Explorer

Theorem necon3d

Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006)

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

Step	Hyp	Ref	Expression
1		necon3d.1	$⊢ φ \to (A = B \to C = D)$
2	1	necon3ad	$⊢ φ \to (C \neq D \to \neg A = B)$
3		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
4	2 3	imbitrrdi	$⊢ φ \to (C \neq D \to A \neq B)$