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

Theorem necon2bbid 2629
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 2573 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6bb 253 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
43con2bid 320 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2571
This theorem is referenced by:  necon4bid  2637  omwordi  6777  omass  6786  nnmwordi  6841  sdom1  7271  pceq0  13203  ftalem5  20816  fsumvma  20954  dchrelbas4  20984  f1otrspeq  27262  pmtrfinv  27274  symggen  27283  psgnunilem1  27288  lkreqN  29657
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 178  df-ne 2573
  Copyright terms: Public domain W3C validator