Theorem necon1abii

Description: Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007) (Proof shortened by Wolf Lammen, 25-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		necon1abii.1	$$⊢\neg \phi \leftrightarrow A=B$$
2		notnotb	$$⊢\phi \leftrightarrow \neg \neg \phi$$
3	1	necon3bbii	$$⊢\neg \neg \phi \leftrightarrow A\ne B$$
4	2 3	bitr2i	$$⊢A\ne B\leftrightarrow \phi$$