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

Theorem necon1bi 2685
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon1bi.1  |-  ( A  =/=  B  ->  ph )
Assertion
Ref Expression
necon1bi  |-  ( -. 
ph  ->  A  =  B )

Proof of Theorem necon1bi
StepHypRef Expression
1 df-ne 2650 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon1bi.1 . . 3  |-  ( A  =/=  B  ->  ph )
31, 2sylbir 213 . 2  |-  ( -.  A  =  B  ->  ph )
43con1i 129 1  |-  ( -. 
ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2648
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 2650
This theorem is referenced by:  necon4ai  2690  fvbr0  5823  peano5  6612  1stnpr  6694  2ndnpr  6695  1st2val  6715  2nd2val  6716  eceqoveq  7318  mapprc  7331  ixp0  7409  setind  8069  hashfun  12321  hashf1lem2  12331  iswrdi  12361  dvdsrval  16870  thlle  18257  konigsberg  23787  hatomistici  25945  setindtr  29544  afvpcfv0  30223
  Copyright terms: Public domain W3C validator