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

Theorem necon1bi 2700
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 2664 . . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon4ai  2705  fvbr0  5892  peano5  6717  1stnpr  6798  2ndnpr  6799  1st2val  6820  2nd2val  6821  eceqoveq  7426  mapprc  7434  ixp0  7512  setind  8175  hashfun  12471  hashf1lem2  12481  iswrdi  12528  dvdsrval  17143  thlle  18574  konigsberg  24778  hatomistici  27072  mppsval  28725  setindtr  30862  fourierdlem72  31770  afvpcfv0  31989
  Copyright terms: Public domain W3C validator