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

Theorem 3netr3d 2751
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 2743 . 2  |-  ( ph  ->  A  =/=  D )
51, 4eqnetrrd 2742 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    =/= wne 2644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-cleq 2443  df-ne 2646
This theorem is referenced by:  subrgnzr  17455  dchrisum0re  22878  pellex  29314  cdlemg9a  34582  cdlemg11aq  34588  cdlemg12b  34594  cdlemg12  34600  cdlemg13  34602  cdlemg19  34634  cdlemk3  34783  cdlemk12  34800  cdlemk12u  34822  lclkrlem2g  35464  mapdncol  35621  mapdpglem29  35651  hdmaprnlem1N  35803  hdmap14lem9  35830
  Copyright terms: Public domain W3C validator