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	⊢ 𝐴 = 𝐵
	neeq12i.2	⊢ 𝐶 = 𝐷
Assertion	neeq12i	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		neeq1i.1	⊢ 𝐴 = 𝐵
2		neeq12i.2	⊢ 𝐶 = 𝐷
3	1 2	eqeq12i	⊢ ( 𝐴 = 𝐶 ↔ 𝐵 = 𝐷 )
4	3	necon3bii	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷 )