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

Theorem necon1bi 2649
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon1bi.1  |-  ( A  =/=  B  ->  ph )
Assertion
Ref Expression
necon1bi  |-  ( -. 
ph  ->  A  =  B )

Proof of Theorem necon1bi
StepHypRef Expression
1 necon1bi.1 . . 3  |-  ( A  =/=  B  ->  ph )
21con3i 130 . 2  |-  ( -. 
ph  ->  -.  A  =/=  B )
3 nne 2607 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3sylib 190 1  |-  ( -. 
ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  peano5  4871  fvbr0  5755  1st2val  6375  2nd2val  6376  eceqoveq  7012  mapprc  7025  ixp0  7098  setind  7676  hashfun  11705  hashf1lem2  11710  iswrdi  11736  dvdsrval  15755  thlle  16929  konigsberg  21714  hatomistici  23870  1stnpr  24098  2ndnpr  24099  setindtr  27109  afvpcfv0  28000  iswrd0i  28201
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator