Theorem 3netr3d 3033

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  subrgnzr  20762  qsnzr  21552  clmopfne  25330  dchrisum0re  27757  prlngsymquadlem  29328  fracfld  33757  dimlssid  34150  algextdeglem4  34238  constrrtll  34249  cdlemg9a  41513  cdlemg11aq  41519  cdlemg12b  41525  cdlemg12  41531  cdlemg13  41533  cdlemg19  41565  cdlemk3  41714  cdlemk12  41731  cdlemk12u  41753  lclkrlem2g  42394  mapdncol  42551  mapdpglem29  42581  hdmaprnlem1N  42730  hdmap14lem9  42757  aks6d1c2p2  42993  ricdrng1  43418  pellex  43684