Theorem 3netr3g

Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012)

	Ref	Expression
Hypotheses	3netr3g.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	3netr3g.2	⊢ 𝐴 = 𝐶
	3netr3g.3	⊢ 𝐵 = 𝐷
Assertion	3netr3g	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		3netr3g.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
2		3netr3g.2	⊢ 𝐴 = 𝐶
3		3netr3g.3	⊢ 𝐵 = 𝐷
4	2 3	neeq12i	⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷 )
5	1 4	sylib	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )