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

Theorem 3netr3d 2857
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 2850 . 2 (𝜑𝐴𝐷)
51, 4eqnetrrd 2849 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  subrgnzr  19037  clmopfne  22651  dchrisum0re  24946  cdlemg9a  34721  cdlemg11aq  34727  cdlemg12b  34733  cdlemg12  34739  cdlemg13  34741  cdlemg19  34773  cdlemk3  34922  cdlemk12  34939  cdlemk12u  34961  lclkrlem2g  35603  mapdncol  35760  mapdpglem29  35790  hdmaprnlem1N  35942  hdmap14lem9  35969  pellex  36200
  Copyright terms: Public domain W3C validator