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

Theorem necon2abid 2516
Description: Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.)
Hypothesis
Ref Expression
necon2abid.1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Assertion
Ref Expression
necon2abid  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )

Proof of Theorem necon2abid
StepHypRef Expression
1 necon2abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
21con2bid 319 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
3 df-ne 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6bbr 254 1  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  sossfld  5136  fin23lem24  7964  isf32lem4  7998  sqgt0sr  8744  leltne  8927  xrleltne  10495  xrltne  10510  ge0nemnf  10518  xlt2add  10596  supxrbnd  10663  supxrre2  10666  ioopnfsup  10984  icopnfsup  10985  xblpnf  17969  nmoreltpnf  21363  nmopreltpnf  22465
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