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

Theorem necon2bbid 2669
Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon2bbid.1  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
Assertion
Ref Expression
necon2bbid  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )

Proof of Theorem necon2bbid
StepHypRef Expression
1 necon2bbid.1 . . 3  |-  ( ph  ->  ( ps  <->  A  =/=  B ) )
2 df-ne 2608 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6bb 261 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
43con2bid 329 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1369    =/= wne 2606
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 2608
This theorem is referenced by:  necon4bid  2677  omwordi  7010  omass  7019  nnmwordi  7074  sdom1  7512  pceq0  13937  f1otrspeq  15953  pmtrfinv  15967  symggen  15976  psgnunilem1  15999  mdetralt  18414  mdetunilem7  18424  ftalem5  22414  fsumvma  22552  dchrelbas4  22582  fsumcvg4  26380  lkreqN  32815
  Copyright terms: Public domain W3C validator