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

Theorem necon2bi 2694
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 2659 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 120 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1395    =/= wne 2652
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 2654
This theorem is referenced by:  necon4iOLD  2702  minel  3885  rzal  3934  difsnb  4174  reusv7OLD  4668  dtrucor2  4690  kmlem6  8552  winainflem  9088  0npi  9277  0npr  9387  0nsr  9473  1div0  10229  rexmul  11488  rennim  13083  mrissmrcd  15056  prmirred  18651  prmirredOLD  18654  pthaus  20264  rplogsumlem2  23795  pntrlog2bndlem4  23890  pntrlog2bndlem5  23891  1div0apr  25302  subfacp1lem6  28804  itg2addnclem3  30230  sdrgacs  31312  rzalf  31553  jumpncnp  31862  fourierswlem  32174  bnj1311  34181  bj-dtrucor2v  34488  cdleme31id  36221
  Copyright terms: Public domain W3C validator