Theorem 3netr3d 3092

Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypotheses

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

Assertion

Ref	Expression
3netr3d	⊢ (𝜑 → 𝐶 ≠ 𝐷)

Proof of Theorem 3netr3d

Step	Hyp	Ref	Expression
1		3netr3d.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3netr3d.1	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
3		3netr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	neeqtrd 3085	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
5	1, 4	eqnetrrd 3084	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-ne 3017

This theorem is referenced by:  subrgnzr  20041  clmopfne  23700  dchrisum0re  26089  cdlemg9a  37783  cdlemg11aq  37789  cdlemg12b  37795  cdlemg12  37801  cdlemg13  37803  cdlemg19  37835  cdlemk3  37984  cdlemk12  38001  cdlemk12u  38023  lclkrlem2g  38664  mapdncol  38821  mapdpglem29  38851  hdmaprnlem1N  39000  hdmap14lem9  39027  pellex  39452