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

Theorem necon4d 2673
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 2661 . 2  |-  ( ph  ->  ( C  =  D  ->  -.  A  =/=  B ) )
3 nne 2648 . 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 1370    =/= wne 2642
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 2644
This theorem is referenced by:  oa00  7095  map0g  7349  epfrs  8049  fin23lem24  8589  abs00  12877  oddvds  16151  isabvd  17008  uvcf1  18323  lindff1  18355  hausnei2  19070  dfcon2  19136  hausflimi  19666  hauspwpwf1  19673  cxpeq0  22236  his6  24633  rpnnen3  29516  01eq0rng  30912  lkreqN  33118  ltrnideq  34122  hdmapip0  35866
  Copyright terms: Public domain W3C validator