Theorem necon3bid

Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005) (Proof shortened by Andrew Salmon, 25-May-2011)

	Ref	Expression
Hypothesis	necon3bid.1	$$⊢\phi \to \left(A=B\leftrightarrow C=D\right)$$
Assertion	necon3bid	$$⊢\phi \to \left(A\ne B\leftrightarrow C\ne D\right)$$

Proof

Step	Hyp	Ref	Expression
1		necon3bid.1	$$⊢\phi \to \left(A=B\leftrightarrow C=D\right)$$
2		df-ne	$$⊢A\ne B\leftrightarrow \neg A=B$$
3	1	necon3bbid	$$⊢\phi \to \left(\neg A=B\leftrightarrow C\ne D\right)$$
4	2 3	syl5bb	$$⊢\phi \to \left(A\ne B\leftrightarrow C\ne D\right)$$