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

Metamath Proof Explorer

Theorem necon3bd

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

		Ref	Expression
	Hypothesis	necon3bd.1	$⊢ φ \to (A = B \to ψ)$
	Assertion	necon3bd	$⊢ φ \to (\neg ψ \to A \neq B)$

Step	Hyp	Ref	Expression
1		necon3bd.1	$⊢ φ \to (A = B \to ψ)$
2		nne	$⊢ \neg A \neq B \leftrightarrow A = B$
3	2 1	biimtrid	$⊢ φ \to (\neg A \neq B \to ψ)$
4	3	con1d	$⊢ φ \to (\neg ψ \to A \neq B)$