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

Theorem necon2bbid 2723
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 291 . . 3  |-  ( ps  <->  -. 
-.  ps )
2 necon2bbid.1 . . 3  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
31, 2syl5rbbr 260 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
-.  ps ) )
43necon4abid 2718 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon4bid  2726  omwordi  7232  omass  7241  nnmwordi  7296  sdom1  7731  pceq0  14269  f1otrspeq  16343  pmtrfinv  16357  symggen  16366  psgnunilem1  16389  mdetralt  18977  mdetunilem7  18987  ftalem5  23214  fsumvma  23352  dchrelbas4  23382  fsumcvg4  27764  lkreqN  34373
  Copyright terms: Public domain W3C validator