Theorem 3netr3d 3032

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 3025	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐷)
5	1, 4	eqnetrrd 3024	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Syntax hints:   → wi 4   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  subrgnzr  20623  clmopfne  25138  dchrisum0re  27554  fracfld  33456  qsnzr  33603  dimlssid  33890  algextdeglem4  33978  constrrtll  33989  cdlemg9a  41220  cdlemg11aq  41226  cdlemg12b  41232  cdlemg12  41238  cdlemg13  41240  cdlemg19  41272  cdlemk3  41421  cdlemk12  41438  cdlemk12u  41460  lclkrlem2g  42101  mapdncol  42258  mapdpglem29  42288  hdmaprnlem1N  42437  hdmap14lem9  42464  aks6d1c2p2  42700  ricdrng1  43110  pellex  43376