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

Theorem necon1d 2673
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 2605 . . 3  |-  ( -.  C  =/=  D  <->  C  =  D )
31, 2syl6ibr 219 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  C  =/=  D
) )
43necon4ad 2665 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  disji  4200  mul02lem2  9243  xblss2ps  18431  xblss2  18432  lgsne0  21117  h1datomi  23083  eigorthi  23340  disjif  24020  lineintmo  26091  2llnmat  30321  2lnat  30581  tendospcanN  31821  dihmeetlem13N  32117  dochkrshp  32184
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 178  df-ne 2601
  Copyright terms: Public domain W3C validator