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

Theorem necon2abid 2702
Description: Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
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 ) )
21necon3abid 2694 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
-.  ps ) )
3 notnot 291 . 2  |-  ( ps  <->  -. 
-.  ps )
42, 3syl6rbbr 264 1  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1370    =/= wne 2644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2646
This theorem is referenced by:  sossfld  5383  fin23lem24  8592  isf32lem4  8626  sqgt0sr  9374  leltne  9565  xrleltne  11223  xrltne  11238  ge0nemnf  11246  xlt2add  11324  supxrbnd  11392  supxrre2  11395  ioopnfsup  11804  icopnfsup  11805  xblpnfps  20086  xblpnf  20087  nmoreltpnf  24304  nmopreltpnf  25408
  Copyright terms: Public domain W3C validator