Theorem neeq12i

Description: Inference for inequality. (Contributed by NM, 24-Jul-2012) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Hypotheses	neeq1i.1	$$⊢A=B$$
	neeq12i.2	$$⊢C=D$$
Assertion	neeq12i	$$⊢A\ne C\leftrightarrow B\ne D$$

Proof

Step	Hyp	Ref	Expression
1		neeq1i.1	$$⊢A=B$$
2		neeq12i.2	$$⊢C=D$$
3	1 2	eqeq12i	$$⊢A=C\leftrightarrow B=D$$
4	3	necon3bii	$$⊢A\ne C\leftrightarrow B\ne D$$