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

Theorem necon2abid 2636
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 2628 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
-.  ps ) )
3 notnot 289 . 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 1399    =/= wne 2577
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 2579
This theorem is referenced by:  sossfld  5363  fin23lem24  8615  isf32lem4  8649  sqgt0sr  9394  leltne  9585  xrleltne  11272  xrltne  11287  ge0nemnf  11295  xlt2add  11373  supxrbnd  11441  supxrre2  11444  ioopnfsup  11891  icopnfsup  11892  xblpnfps  20983  xblpnf  20984  nmoreltpnf  25801  nmopreltpnf  26904  elprneb  32464
  Copyright terms: Public domain W3C validator