Theorem necon3abii

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

	Ref	Expression
Hypothesis	necon3abii.1	$$⊢A=B\leftrightarrow \phi$$
Assertion	necon3abii	$$⊢A\ne B\leftrightarrow \neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		necon3abii.1	$$⊢A=B\leftrightarrow \phi$$
2		df-ne	$$⊢A\ne B\leftrightarrow \neg A=B$$
3	2 1	xchbinx	$$⊢A\ne B\leftrightarrow \neg \phi$$