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

Theorem necon1bi 2851
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 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bi.1 . . 3 (𝐴𝐵𝜑)
31, 2sylbir 225 . 2 𝐴 = 𝐵𝜑)
43con1i 144 1 𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon4ai  2854  fvbr0  6253  peano5  7131  1stnpr  7214  2ndnpr  7215  1st2val  7238  2nd2val  7239  eceqoveq  7895  mapprc  7903  ixp0  7983  setind  8648  hashfun  13262  hashf1lem2  13278  iswrdi  13341  dvdsrval  18691  thlle  20089  konigsberg  27235  hatomistici  29349  esumrnmpt2  30258  mppsval  31595  setindtr  37908  fourierdlem72  40713  afvpcfv0  41547
  Copyright terms: Public domain W3C validator