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

Theorem 3netr3d 3013
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 3006 . 2 (𝜑𝐴𝐷)
51, 4eqnetrrd 3005 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wne 2937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-ne 2938
This theorem is referenced by:  subrgnzr  19542  clmopfne  23174  dchrisum0re  25493  cdlemg9a  36588  cdlemg11aq  36594  cdlemg12b  36600  cdlemg12  36606  cdlemg13  36608  cdlemg19  36640  cdlemk3  36789  cdlemk12  36806  cdlemk12u  36828  lclkrlem2g  37469  mapdncol  37626  mapdpglem29  37656  hdmaprnlem1N  37805  hdmap14lem9  37832  pellex  38077
  Copyright terms: Public domain W3C validator