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

Theorem necon4d 2509
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 2495 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2450 . 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 1623    =/= wne 2446
This theorem is referenced by:  oa00  6557  map0g  6807  epfrs  7413  fin23lem24  7948  abs00  11774  oddvds  14862  isabvd  15585  hausnei2  17081  dfcon2  17145  hausflimi  17675  hauspwpwf1  17682  cxpeq0  20025  his6  21678  rpnnen3  27125  uvcf1  27241  lindff1  27290  lkreqN  29360  ltrnideq  30364  hdmapip0  32108
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 2448
  Copyright terms: Public domain W3C validator