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

Theorem necon1bi 2641
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 2602 . 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 1652    =/= wne 2598
This theorem is referenced by:  peano5  4860  fvbr0  5744  1st2val  6364  2nd2val  6365  eceqoveq  7001  mapprc  7014  ixp0  7087  setind  7665  hashfun  11692  hashf1lem2  11697  iswrdi  11723  dvdsrval  15742  thlle  16916  konigsberg  21701  hatomistici  23857  1stnpr  24085  2ndnpr  24086  setindtr  27086  afvpcfv0  27977  iswrd0i  28146
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 2600
  Copyright terms: Public domain W3C validator