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

Theorem 3netr3d 2485
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 2474 . 2  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
51, 4mpbid 201 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  subrgnzr  16035  dchrisum0re  20678  pellex  27023  cdlemg9a  31443  cdlemg11aq  31449  cdlemg12b  31455  cdlemg12  31461  cdlemg13  31463  cdlemg19  31495  cdlemk3  31644  cdlemk12  31661  cdlemk12u  31683  lclkrlem2g  32325  mapdncol  32482  mapdpglem29  32512  hdmaprnlem1N  32664  hdmap14lem9  32691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator