Theorem 3netr3d 3034

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  subrgnzr  20680  qsnzr  21464  clmopfne  25236  dchrisum0re  27655  prlngsymquadlem  29191  fracfld  33607  dimlssid  34000  algextdeglem4  34088  constrrtll  34099  cdlemg9a  41384  cdlemg11aq  41390  cdlemg12b  41396  cdlemg12  41402  cdlemg13  41404  cdlemg19  41436  cdlemk3  41585  cdlemk12  41602  cdlemk12u  41624  lclkrlem2g  42265  mapdncol  42422  mapdpglem29  42452  hdmaprnlem1N  42601  hdmap14lem9  42628  aks6d1c2p2  42864  ricdrng1  43276  pellex  43542