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

Theorem necon2bi 2661
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 2625 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 123 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2618
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 188  df-ne 2620
This theorem is referenced by:  necon4iOLD  2669  minel  3848  rzal  3899  difsnb  4139  dtrucor2  4652  kmlem6  8586  winainflem  9119  0npi  9308  0npr  9418  0nsr  9504  1div0  10272  rexmul  11558  rennim  13291  mrissmrcd  15534  prmirred  19053  pthaus  20640  rplogsumlem2  24310  pntrlog2bndlem4  24405  pntrlog2bndlem5  24406  1div0apr  25891  bnj1311  29829  subfacp1lem6  29904  bj-dtrucor2v  31374  itg2addnclem3  31909  cdleme31id  33880  sdrgacs  35987  rzalf  37199  jumpncnp  37596  fourierswlem  37914
  Copyright terms: Public domain W3C validator