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

Theorem necon2bi 2689
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
Hypothesis
Ref Expression
necon2bi.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necon2bi  |-  ( A  =  B  ->  -.  ph )

Proof of Theorem necon2bi
StepHypRef Expression
1 necon2bi.1 . . 3  |-  ( ph  ->  A  =/=  B )
21neneqd 2655 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 120 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2648
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 2650
This theorem is referenced by:  necon4iOLD  2697  minel  3843  rzal  3890  difsnb  4124  reusv7OLD  4613  dtrucor2  4635  kmlem6  8436  winainflem  8972  0npi  9163  0npr  9273  0nsr  9358  renfdisj  9549  1div0  10107  rexmul  11346  rennim  12847  mrissmrcd  14698  prmirred  18045  prmirredOLD  18048  pthaus  19344  rplogsumlem2  22868  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  1div0apr  23814  subfacp1lem6  27218  itg2addnclem3  28594  sdrgacs  29707  rzalf  29888  bnj1311  32348  bj-dtrucor2v  32655  cdleme31id  34377
  Copyright terms: Public domain W3C validator