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

Theorem 3netr4d 2486
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
Hypotheses
Ref Expression
3netr4d.1  |-  ( ph  ->  A  =/=  B )
3netr4d.2  |-  ( ph  ->  C  =  A )
3netr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3netr4d  |-  ( ph  ->  C  =/=  D )

Proof of Theorem 3netr4d
StepHypRef Expression
1 3netr4d.1 . 2  |-  ( ph  ->  A  =/=  B )
2 3netr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3netr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3neeq12d 2474 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  infpssrlem4  7948  isdrng2  15538  prmirredlem  16462  dfac14lem  17327  i1fmullem  19065  fta1glem1  19567  fta1blem  19570  plydivlem4  19692  fta1lem  19703  cubic  20161  asinlem  20180  dchrn0  20505  lgsne0  20588  subfacp1lem5  23730  nofulllem4  24430  axlowdimlem14  24655  fvtransport  24727  uvcf1  27344  dalem4  30476  cdleme35sn2aw  31269  cdleme39n  31277  cdleme41fva11  31288  trlcone  31539  hdmap1neglem1N  32640  hdmaprnlem3N  32665
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