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

Theorem 3netr3d 3017
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 3010 . 2 (𝜑𝐴𝐷)
51, 4eqnetrrd 3009 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  subrgnzr  20594  clmopfne  25129  dchrisum0re  27557  fracfld  33310  qsnzr  33483  dimlssid  33683  algextdeglem4  33761  constrrtll  33772  cdlemg9a  40634  cdlemg11aq  40640  cdlemg12b  40646  cdlemg12  40652  cdlemg13  40654  cdlemg19  40686  cdlemk3  40835  cdlemk12  40852  cdlemk12u  40874  lclkrlem2g  41515  mapdncol  41672  mapdpglem29  41702  hdmaprnlem1N  41851  hdmap14lem9  41878  aks6d1c2p2  42120  ricdrng1  42538  pellex  42846
  Copyright terms: Public domain W3C validator