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

Theorem necon2bi 2665
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 2639 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 125 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1454    =/= wne 2632
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 190  df-ne 2634
This theorem is referenced by:  minel  3831  rzal  3882  difsnb  4126  dtrucor2  4647  kmlem6  8610  winainflem  9143  0npi  9332  0npr  9442  0nsr  9528  1div0  10298  rexmul  11585  rennim  13350  mrissmrcd  15594  prmirred  19114  pthaus  20701  rplogsumlem2  24371  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  1div0apr  25953  bnj1311  29881  subfacp1lem6  29956  bj-dtrucor2v  31460  itg2addnclem3  32039  cdleme31id  34005  sdrgacs  36111  rzalf  37377  jumpncnp  37813  fourierswlem  38131
  Copyright terms: Public domain W3C validator