Theorem 3netr3d 3008

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

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

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 2708

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

This theorem is referenced by:  subrgnzr  20527  clmopfne  25052  dchrisum0re  27480  fracfld  33390  qsnzr  33536  dimlssid  33789  algextdeglem4  33877  constrrtll  33888  cdlemg9a  40888  cdlemg11aq  40894  cdlemg12b  40900  cdlemg12  40906  cdlemg13  40908  cdlemg19  40940  cdlemk3  41089  cdlemk12  41106  cdlemk12u  41128  lclkrlem2g  41769  mapdncol  41926  mapdpglem29  41956  hdmaprnlem1N  42105  hdmap14lem9  42132  aks6d1c2p2  42369  ricdrng1  42779  pellex  43073