Theorem 3netr3d 2760

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 2752	. 2
5	1, 4	eqnetrrd 2751	1

Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652

This theorem is referenced by:  subrgnzr  17916  dchrisum0re  23698  pellex  30771  cdlemg9a  36358  cdlemg11aq  36364  cdlemg12b  36370  cdlemg12  36376  cdlemg13  36378  cdlemg19  36410  cdlemk3  36559  cdlemk12  36576  cdlemk12u  36598  lclkrlem2g  37240  mapdncol  37397  mapdpglem29  37427  hdmaprnlem1N  37579  hdmap14lem9  37606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654