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

Theorem necon2bbid 2504
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 2448 . . 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 1623    =/= wne 2446
This theorem is referenced by:  necon4bid  2512  omwordi  6569  omass  6578  nnmwordi  6633  sdom1  7062  pceq0  12923  ftalem5  20314  fsumvma  20452  dchrelbas4  20482  f1otrspeq  27390  pmtrfinv  27402  symggen  27411  psgnunilem1  27416  lkreqN  29360
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 2448
  Copyright terms: Public domain W3C validator