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

Theorem necon4bd 2613
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 2555 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon4bd.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
32con1d 118 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  ps )
)
41, 3syl5bir 210 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2551
This theorem is referenced by:  om00  6755  pw2f1olem  7149  xlt2add  10772  hashtpg  11619  hashfun  11628  fsumcl2lem  12453  gcdeq0  12949  phibndlem  13087  abvn0b  16290  cfinufil  17882  isxmet2d  18267  i1fres  19465  tdeglem4  19851  ply1domn  19914  pilem2  20236  isnsqf  20786  ppieq0  20827  chpeq0  20860  chteq0  20861  fprodcl2lem  25056  ltrnatlw  30298
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 2553
  Copyright terms: Public domain W3C validator