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	|- ( ph <-> ( ps /\ A =/= B ) )
	bnj1541.2	|- -. ph
Assertion	bnj1541	|- ( ps -> A = B )

Proof

Step	Hyp	Ref	Expression
1		bnj1541.1	|- ( ph <-> ( ps /\ A =/= B ) )
2		bnj1541.2	|- -. ph
3	2 1	mtbi	|- -. ( ps /\ A =/= B )
4	3	imnani	|- ( ps -> -. A =/= B )
5		nne	|- ( -. A =/= B <-> A = B )
6	4 5	sylib	|- ( ps -> A = B )