Theorem 3netr3d 3016

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2939

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2940

This theorem is referenced by:  subrgnzr  20492  clmopfne  24943  dchrisum0re  27359  qsnzr  33014  algextdeglem4  33231  cdlemg9a  39967  cdlemg11aq  39973  cdlemg12b  39979  cdlemg12  39985  cdlemg13  39987  cdlemg19  40019  cdlemk3  40168  cdlemk12  40185  cdlemk12u  40207  lclkrlem2g  40848  mapdncol  41005  mapdpglem29  41035  hdmaprnlem1N  41184  hdmap14lem9  41211  aks6d1c2p2  41424  ricdrng1  41567  pellex  42036