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

Theorem 3netr3d 2727
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 2719 . 2  |-  ( ph  ->  A  =/=  D )
51, 4eqnetrrd 2718 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    =/= wne 2618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2620
This theorem is referenced by:  subrgnzr  18479  dchrisum0re  24337  cdlemg9a  34117  cdlemg11aq  34123  cdlemg12b  34129  cdlemg12  34135  cdlemg13  34137  cdlemg19  34169  cdlemk3  34318  cdlemk12  34335  cdlemk12u  34357  lclkrlem2g  34999  mapdncol  35156  mapdpglem29  35186  hdmaprnlem1N  35338  hdmap14lem9  35365  pellex  35598
  Copyright terms: Public domain W3C validator