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

Theorem necon1bi 2614
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 129 . 2  |-  ( -. 
ph  ->  -.  A  =/=  B )
3 nne 2575 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3sylib 189 1  |-  ( -. 
ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2571
This theorem is referenced by:  peano5  4831  fvbr0  5715  1st2val  6335  2nd2val  6336  eceqoveq  6972  mapprc  6985  ixp0  7058  setind  7633  hashfun  11659  hashf1lem2  11664  iswrdi  11690  dvdsrval  15709  thlle  16883  konigsberg  21666  hatomistici  23822  1stnpr  24050  2ndnpr  24051  setindtr  26989  afvpcfv0  27881  iswrd0i  28003
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 2573
  Copyright terms: Public domain W3C validator