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

Theorem necon1bi 2674
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 2638 . . 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 1381    =/= wne 2636
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 2638
This theorem is referenced by:  necon4ai  2679  fvbr0  5873  peano5  6704  1stnpr  6785  2ndnpr  6786  1st2val  6807  2nd2val  6808  eceqoveq  7414  mapprc  7422  ixp0  7500  setind  8163  hashfun  12469  hashf1lem2  12479  iswrdi  12526  dvdsrval  17162  thlle  18595  konigsberg  24852  hatomistici  27146  mppsval  28798  setindtr  30934  fourierdlem72  31846  afvpcfv0  32065
  Copyright terms: Public domain W3C validator