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

Theorem necon2abid 2503
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 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  sossfld  5120  fin23lem24  7948  isf32lem4  7982  sqgt0sr  8728  leltne  8911  xrleltne  10479  xrltne  10494  ge0nemnf  10502  xlt2add  10580  supxrbnd  10647  supxrre2  10650  ioopnfsup  10968  icopnfsup  10969  xblpnf  17953  nmoreltpnf  21347  nmopreltpnf  22449
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 2448
  Copyright terms: Public domain W3C validator