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

Theorem necon2abid 2608
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 320 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
3 df-ne 2553 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6bbr 255 1  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2551
This theorem is referenced by:  sossfld  5258  fin23lem24  8136  isf32lem4  8170  sqgt0sr  8915  leltne  9098  xrleltne  10671  xrltne  10686  ge0nemnf  10694  xlt2add  10772  supxrbnd  10840  supxrre2  10843  ioopnfsup  11173  icopnfsup  11174  xblpnf  18328  nmoreltpnf  22119  nmopreltpnf  23221
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