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

Theorem necon2bbid 2579
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 2523 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6bb 252 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
43con2bid 319 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1642    =/= wne 2521
This theorem is referenced by:  necon4bid  2587  omwordi  6653  omass  6662  nnmwordi  6717  sdom1  7147  pceq0  13014  ftalem5  20420  fsumvma  20558  dchrelbas4  20588  f1otrspeq  26713  pmtrfinv  26725  symggen  26734  psgnunilem1  26739  lkreqN  29412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2523
  Copyright terms: Public domain W3C validator