Theorem 3netr3d 3005

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  subrgnzr  20511  clmopfne  25024  dchrisum0re  27452  fracfld  33281  qsnzr  33427  dimlssid  33666  algextdeglem4  33754  constrrtll  33765  cdlemg9a  40751  cdlemg11aq  40757  cdlemg12b  40763  cdlemg12  40769  cdlemg13  40771  cdlemg19  40803  cdlemk3  40952  cdlemk12  40969  cdlemk12u  40991  lclkrlem2g  41632  mapdncol  41789  mapdpglem29  41819  hdmaprnlem1N  41968  hdmap14lem9  41995  aks6d1c2p2  42232  ricdrng1  42646  pellex  42952