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

Theorem necon1bi 3005
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 2978 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bi.1 . . 3 (𝐴𝐵𝜑)
31, 2sylbir 226 . 2 𝐴 = 𝐵𝜑)
43con1i 146 1 𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1637  wne 2977
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 198  df-ne 2978
This theorem is referenced by:  necon4ai  3008  fvbr0  6432  peano5  7316  1stnpr  7399  2ndnpr  7400  1st2val  7423  2nd2val  7424  eceqoveq  8085  mapprc  8093  ixp0  8175  setind  8854  hashfun  13437  hashf1lem2  13453  iswrdi  13516  dvdsrval  18843  thlle  20247  konigsberg  27426  hatomistici  29546  esumrnmpt2  30452  mppsval  31789  setindtr  38089  fourierdlem72  40871  afvpcfv0  41732
  Copyright terms: Public domain W3C validator