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

Theorem necon4bd 2521
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 2463 . 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 1632    =/= wne 2459
This theorem is referenced by:  om00  6589  pw2f1olem  6982  xlt2add  10596  hashfun  11405  fsumcl2lem  12220  gcdeq0  12716  phibndlem  12854  abvn0b  16059  cfinufil  17639  isxmet2d  17908  i1fres  19076  tdeglem4  19462  ply1domn  19525  pilem2  19844  isnsqf  20389  ppieq0  20430  chpeq0  20463  chteq0  20464  hashtpg  28217  ltrnatlw  30994
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