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

Theorem necon1bi 2961
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 (𝐴𝐵𝜑)
Assertion
Ref Expression
necon1bi 𝜑𝐴 = 𝐵)

Proof of Theorem necon1bi
StepHypRef Expression
1 df-ne 2933 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bi.1 . . 3 (𝐴𝐵𝜑)
31, 2sylbir 234 . 2 𝐴 = 𝐵𝜑)
43con1i 147 1 𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wne 2932
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 206  df-ne 2933
This theorem is referenced by:  necon4ai  2964  iotanul2  6503  fvbr0  6910  peano5  7877  peano5OLD  7878  1stnpr  7972  2ndnpr  7973  1st2val  7996  2nd2val  7997  eceqoveq  8811  mapprc  8819  ixp0  8920  cnvfi  9175  setind  9724  hashfun  14393  hashf1lem2  14413  iswrdi  14464  ffz0iswrd  14487  dvdsrval  20248  thlle  21551  thlleOLD  21552  konigsberg  29934  hatomistici  32039  esumrnmpt2  33521  mppsval  35018  setindtr  42218  fourierdlem72  45345  afvpcfv0  46305
  Copyright terms: Public domain W3C validator