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

Theorem necon4d 2522
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon4d.1  |-  ( ph  ->  ( A  =/=  B  ->  C  =/=  D ) )
Assertion
Ref Expression
necon4d  |-  ( ph  ->  ( C  =  D  ->  A  =  B ) )

Proof of Theorem necon4d
StepHypRef Expression
1 necon4d.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  C  =/=  D ) )
21necon2bd 2508 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2463 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 217 1  |-  ( ph  ->  ( C  =  D  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  oa00  6573  map0g  6823  epfrs  7429  fin23lem24  7964  abs00  11790  oddvds  14878  isabvd  15601  hausnei2  17097  dfcon2  17161  hausflimi  17691  hauspwpwf1  17698  cxpeq0  20041  his6  21694  rpnnen3  27228  uvcf1  27344  lindff1  27393  lkreqN  29982  ltrnideq  30986  hdmapip0  32730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2461
  Copyright terms: Public domain W3C validator