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

Theorem necon4d 2669
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 2655 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2607 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 219 1  |-  ( ph  ->  ( C  =  D  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  oa00  6804  map0g  7055  epfrs  7669  fin23lem24  8204  abs00  12096  oddvds  15187  isabvd  15910  hausnei2  17419  dfcon2  17484  hausflimi  18014  hauspwpwf1  18021  cxpeq0  20571  his6  22603  rpnnen3  27105  uvcf1  27220  lindff1  27269  lkreqN  30030  ltrnideq  31034  hdmapip0  32778
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator