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

Theorem necon2bi 2644
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 2614 . 2  |-  ( ph  ->  -.  A  =  B )
32con2i 114 1  |-  ( A  =  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon4i  2658  minel  3675  rzal  3721  difsnb  3932  dtrucor2  4390  reusv7OLD  4727  riotaundb  6583  kmlem6  8025  winainflem  8558  0npi  8749  0npr  8859  0nsr  8944  renfdisj  9128  1div0  9669  rexmul  10840  rennim  12034  mrissmrcd  13855  prmirred  16765  pthaus  17660  rplogsumlem2  21169  pntrlog2bndlem4  21264  pntrlog2bndlem5  21265  1div0apr  21752  subfacp1lem6  24861  itg2addnclem3  26221  sdrgacs  27441  rzalf  27619  bnj1311  29294  cdleme31id  31092
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2600
  Copyright terms: Public domain W3C validator