Theorem 3netr3d 3011

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  subrgnzr  20573  clmopfne  25088  dchrisum0re  27501  fracfld  33399  qsnzr  33545  dimlssid  33823  algextdeglem4  33911  constrrtll  33922  cdlemg9a  41131  cdlemg11aq  41137  cdlemg12b  41143  cdlemg12  41149  cdlemg13  41151  cdlemg19  41183  cdlemk3  41332  cdlemk12  41349  cdlemk12u  41371  lclkrlem2g  42012  mapdncol  42169  mapdpglem29  42199  hdmaprnlem1N  42348  hdmap14lem9  42375  aks6d1c2p2  42611  ricdrng1  43021  pellex  43287