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

Theorem necon1d 2528
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 2463 . . 3  |-  ( -.  C  =/=  D  <->  C  =  D )
31, 2syl6ibr 218 . 2  |-  ( ph  ->  ( A  =/=  B  ->  -.  C  =/=  D
) )
43necon4ad 2520 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  disji  4027  mul02lem2  9005  xblss2  17974  lgsne0  20588  h1datomi  22176  eigorthi  22433  disjif  23370  disjif2  23373  lineintmo  24852  2llnmat  30335  2lnat  30595  tendospcanN  31835  dihmeetlem13N  32131  dochkrshp  32198
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 2461
  Copyright terms: Public domain W3C validator