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

Theorem necon2bbid 2668
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 2607 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6bb 254 . 2  |-  ( ph  ->  ( ps  <->  -.  A  =  B ) )
43con2bid 321 1  |-  ( ph  ->  ( A  =  B  <->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    = wceq 1653    =/= wne 2605
This theorem is referenced by:  necon4bid  2676  omwordi  6843  omass  6852  nnmwordi  6907  sdom1  7337  pceq0  13275  ftalem5  20890  fsumvma  21028  dchrelbas4  21058  f1otrspeq  27405  pmtrfinv  27417  symggen  27426  psgnunilem1  27431  lkreqN  30066
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 179  df-ne 2607
  Copyright terms: Public domain W3C validator