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

Theorem necon4d 2648
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 2640 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2628 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 230 1  |-  ( ph  ->  ( C  =  D  ->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1444    =/= wne 2622
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 189  df-ne 2624
This theorem is referenced by:  oa00  7260  map0g  7511  epfrs  8215  fin23lem24  8752  abs00  13352  oddvds  17196  isabvd  18048  01eq0ring  18496  uvcf1  19350  lindff1  19378  hausnei2  20369  dfcon2  20434  hausflimi  20995  hauspwpwf1  21002  cxpeq0  23623  his6  26752  nn0sqeq1  28324  lkreqN  32736  ltrnideq  33741  hdmapip0  35486  rpnnen3  35887
  Copyright terms: Public domain W3C validator