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

Theorem necon1bi 2564
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 127 . 2  |-  ( -. 
ph  ->  -.  A  =/=  B )
3 nne 2525 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3sylib 188 1  |-  ( -. 
ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1642    =/= wne 2521
This theorem is referenced by:  peano5  4758  fvbr0  5629  1st2val  6229  2nd2val  6230  eceqoveq  6848  mapprc  6861  ixp0  6934  setind  7506  hashfun  11479  hashf1lem2  11484  iswrdi  11507  dvdsrval  15520  thlle  16697  hatomistici  23050  1stnpr  23294  2ndnpr  23295  konigsberg  24315  setindtr  26440  afvpcfv0  27334
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 177  df-ne 2523
  Copyright terms: Public domain W3C validator