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

Theorem 3netr3d 2727
 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 2719 . 2
51, 4eqnetrrd 2718 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wne 2618 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2620 This theorem is referenced by:  subrgnzr  18479  dchrisum0re  24337  cdlemg9a  34117  cdlemg11aq  34123  cdlemg12b  34129  cdlemg12  34135  cdlemg13  34137  cdlemg19  34169  cdlemk3  34318  cdlemk12  34335  cdlemk12u  34357  lclkrlem2g  34999  mapdncol  35156  mapdpglem29  35186  hdmaprnlem1N  35338  hdmap14lem9  35365  pellex  35598
 Copyright terms: Public domain W3C validator