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

Theorem necon2bbid 2678
Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
Hypothesis
Ref Expression
necon2bbid.1  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
Assertion
Ref Expression
necon2bbid  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )

Proof of Theorem necon2bbid
StepHypRef Expression
1 notnot 297 . . 3  |-  ( ps  <->  -. 
-.  ps )
2 necon2bbid.1 . . 3  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
31, 2syl5rbbr 268 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
-.  ps ) )
43necon4abid 2675 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    = wceq 1454    =/= wne 2632
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 190  df-ne 2634
This theorem is referenced by:  necon4bid  2680  omwordi  7297  omass  7306  nnmwordi  7361  sdom1  7797  pceq0  14868  f1otrspeq  17136  pmtrfinv  17150  symggen  17159  psgnunilem1  17182  mdetralt  19681  mdetunilem7  19691  ftalem5  24049  ftalem5OLD  24051  fsumvma  24189  dchrelbas4  24219  fsumcvg4  28804  lkreqN  32780
  Copyright terms: Public domain W3C validator