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

Theorem necon1d 2515
Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1d.1  |-  ( ph  ->  ( A  =/=  B  ->  C  =  D ) )
Assertion
Ref Expression
necon1d  |-  ( ph  ->  ( C  =/=  D  ->  A  =  B ) )

Proof of Theorem necon1d
StepHypRef Expression
1 necon1d.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  C  =  D ) )
2 nne 2450 . . 3  |-  ( -.  C  =/=  D  <->  C  =  D )
31, 2syl6ibr 218 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  C  =/=  D
) )
43necon4ad 2507 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:  disji  4011  mul02lem2  8989  xblss2  17958  lgsne0  20572  h1datomi  22160  eigorthi  22417  disjif  23355  disjif2  23358  lineintmo  24780  2llnmat  29713  2lnat  29973  tendospcanN  31213  dihmeetlem13N  31509  dochkrshp  31576
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