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

Theorem necon1bi 2644
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 135 . 2  |-  ( -. 
ph  ->  -.  A  =/=  B )
3 nne 2602 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3sylib 196 1  |-  ( -. 
ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1362    =/= wne 2596
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 185  df-ne 2598
This theorem is referenced by:  fvbr0  5699  peano5  6488  1stnpr  6570  2ndnpr  6571  1st2val  6591  2nd2val  6592  eceqoveq  7193  mapprc  7206  ixp0  7284  setind  7942  hashfun  12182  hashf1lem2  12192  iswrdi  12222  dvdsrval  16670  thlle  17963  konigsberg  23430  hatomistici  25588  setindtr  29215  afvpcfv0  29895
  Copyright terms: Public domain W3C validator