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

Theorem necon4bd 2663
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon4bd.1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Assertion
Ref Expression
necon4bd  |-  ( ph  ->  ( A  =  B  ->  ps ) )

Proof of Theorem necon4bd
StepHypRef Expression
1 nne 2602 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon4bd.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
32con1d 124 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
41, 3syl5bir 218 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1362    =/= wne 2596
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 2598
This theorem is referenced by:  om00  7002  pw2f1olem  7403  xlt2add  11211  hashtpg  12170  hashfun  12183  fsumcl2lem  13192  gcdeq0  13688  phibndlem  13828  abvn0b  17296  cfinufil  19343  isxmet2d  19744  i1fres  21025  tdeglem4  21414  ply1domn  21480  pilem2  21802  isnsqf  22358  ppieq0  22399  chpeq0  22432  chteq0  22433  fprodcl2lem  27310  ltrnatlw  33421
  Copyright terms: Public domain W3C validator