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

Theorem necon1bi 2489
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 2450 . 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 1623    =/= wne 2446
This theorem is referenced by:  peano5  4679  fvbr0  5549  1st2val  6145  2nd2val  6146  eceqoveq  6763  mapprc  6776  ixp0  6849  setind  7419  hashfun  11389  hashf1lem2  11394  iswrdi  11417  dvdsrval  15427  thlle  16597  hatomistici  22942  1stnpr  23245  2ndnpr  23246  konigsberg  23911  setindtr  27117  afvpcfv0  28009
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 2448
  Copyright terms: Public domain W3C validator