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

Theorem necon2abid 2655
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 2600 . 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 1652    =/= wne 2598
This theorem is referenced by:  sossfld  5309  fin23lem24  8194  isf32lem4  8228  sqgt0sr  8973  leltne  9156  xrleltne  10730  xrltne  10745  ge0nemnf  10753  xlt2add  10831  supxrbnd  10899  supxrre2  10902  ioopnfsup  11237  icopnfsup  11238  xblpnfps  18417  xblpnf  18418  nmoreltpnf  22262  nmopreltpnf  23364
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