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

Metamath Proof Explorer

Theorem bnj1541

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1541.1	$⊢ φ \leftrightarrow (ψ \land A \neq B)$
	bnj1541.2	$⊢ \neg φ$
Assertion	bnj1541	$⊢ ψ \to A = B$

Step	Hyp	Ref	Expression
1		bnj1541.1	$⊢ φ \leftrightarrow (ψ \land A \neq B)$
2		bnj1541.2	$⊢ \neg φ$
3	2 1	mtbi	$⊢ \neg (ψ \land A \neq B)$
4	3	imnani	$⊢ ψ \to \neg A \neq B$
5		nne	$⊢ \neg A \neq B \leftrightarrow A = B$
6	4 5	sylib	$⊢ ψ \to A = B$