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

Theorem necon4bd 2660
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 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 1652    =/= wne 2598
This theorem is referenced by:  om00  6810  pw2f1olem  7204  xlt2add  10831  hashtpg  11683  hashfun  11692  fsumcl2lem  12517  gcdeq0  13013  phibndlem  13151  abvn0b  16354  cfinufil  17952  isxmet2d  18349  i1fres  19589  tdeglem4  19975  ply1domn  20038  pilem2  20360  isnsqf  20910  ppieq0  20951  chpeq0  20984  chteq0  20985  fprodcl2lem  25268  ltrnatlw  30907
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 2600
  Copyright terms: Public domain W3C validator