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

Theorem necon4d 2684
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 2672 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2658 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 226 1  |-  ( ph  ->  ( C  =  D  ->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1395    =/= wne 2652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2654
This theorem is referenced by:  oa00  7226  map0g  7477  epfrs  8179  fin23lem24  8719  abs00  13134  oddvds  16698  isabvd  17596  01eq0ring  18047  uvcf1  18950  lindff1  18982  hausnei2  19981  dfcon2  20046  hausflimi  20607  hauspwpwf1  20614  cxpeq0  23185  his6  26143  nn0sqeq1  27719  rpnnen3  31178  lkreqN  35038  ltrnideq  36043  hdmapip0  37788
  Copyright terms: Public domain W3C validator