MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3netr3d Unicode version

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
StepHypRef Expression
1 3netr3d.2 . 2
2 3netr3d.1 . . 3
3 3netr3d.3 . . 3
42, 3neeqtrd 2752 . 2
51, 4eqnetrrd 2751 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator