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

Metamath Proof Explorer

Theorem necon3abid

Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007)

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

Step	Hyp	Ref	Expression
1		necon3abid.1	$⊢ φ \to (A = B \leftrightarrow ψ)$
2		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
3	1	notbid	$⊢ φ \to (\neg A = B \leftrightarrow \neg ψ)$
4	2 3	bitrid	$⊢ φ \to (A \neq B \leftrightarrow \neg ψ)$