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

Theorem necon4bd 2508
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 2450 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon4bd.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
32con1d 116 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
41, 3syl5bir 209 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  om00  6573  pw2f1olem  6966  xlt2add  10580  hashfun  11389  fsumcl2lem  12204  gcdeq0  12700  phibndlem  12838  abvn0b  16043  cfinufil  17623  isxmet2d  17892  i1fres  19060  tdeglem4  19446  ply1domn  19509  pilem2  19828  isnsqf  20373  ppieq0  20414  chpeq0  20447  chteq0  20448  ltrnatlw  30372
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