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

Theorem 3netr3d 2757
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  |-  ( ph  ->  A  =/=  B )
3netr3d.2  |-  ( ph  ->  A  =  C )
3netr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3netr3d  |-  ( ph  ->  C  =/=  D )

Proof of Theorem 3netr3d
StepHypRef Expression
1 3netr3d.2 . 2  |-  ( ph  ->  A  =  C )
2 3netr3d.1 . . 3  |-  ( ph  ->  A  =/=  B )
3 3netr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3neeqtrd 2749 . 2  |-  ( ph  ->  A  =/=  D )
51, 4eqnetrrd 2748 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651
This theorem is referenced by:  subrgnzr  18114  dchrisum0re  23899  pellex  31013  cdlemg9a  36774  cdlemg11aq  36780  cdlemg12b  36786  cdlemg12  36792  cdlemg13  36794  cdlemg19  36826  cdlemk3  36975  cdlemk12  36992  cdlemk12u  37014  lclkrlem2g  37656  mapdncol  37813  mapdpglem29  37843  hdmaprnlem1N  37995  hdmap14lem9  38022
  Copyright terms: Public domain W3C validator