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

Theorem 3netr3d 3096
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 3089 . 2 (𝜑𝐴𝐷)
51, 4eqnetrrd 3088 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wne 3020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818  df-ne 3021
This theorem is referenced by:  subrgnzr  19963  clmopfne  23618  dchrisum0re  26006  cdlemg9a  37638  cdlemg11aq  37644  cdlemg12b  37650  cdlemg12  37656  cdlemg13  37658  cdlemg19  37690  cdlemk3  37839  cdlemk12  37856  cdlemk12u  37878  lclkrlem2g  38519  mapdncol  38676  mapdpglem29  38706  hdmaprnlem1N  38855  hdmap14lem9  38882  pellex  39300
  Copyright terms: Public domain W3C validator