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

Metamath Proof Explorer

Theorem necon2ad

Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 23-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		necon2ad.1	$⊢ φ \to (A = B \to \neg ψ)$
2		notnot	$⊢ ψ \to \neg \neg ψ$
3	1	necon3bd	$⊢ φ \to (\neg \neg ψ \to A \neq B)$
4	2 3	syl5	$⊢ φ \to (ψ \to A \neq B)$