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

Theorem 3netr3d 2629
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
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.1 . 2  |-  ( ph  ->  A  =/=  B )
2 3netr3d.2 . . 3  |-  ( ph  ->  A  =  C )
3 3netr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3neeq12d 2618 . 2  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
51, 4mpbid 203 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  subrgnzr  16340  dchrisum0re  21209  pellex  26900  cdlemg9a  31491  cdlemg11aq  31497  cdlemg12b  31503  cdlemg12  31509  cdlemg13  31511  cdlemg19  31543  cdlemk3  31692  cdlemk12  31709  cdlemk12u  31731  lclkrlem2g  32373  mapdncol  32530  mapdpglem29  32560  hdmaprnlem1N  32712  hdmap14lem9  32739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator