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

Theorem necon1bi 3044
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 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bi.1 . . 3 (𝐴𝐵𝜑)
31, 2sylbir 236 . 2 𝐴 = 𝐵𝜑)
43con1i 149 1 𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon4ai  3047  fvbr0  6691  peano5  7593  1stnpr  7684  2ndnpr  7685  1st2val  7708  2nd2val  7709  eceqoveq  8392  mapprc  8400  ixp0  8484  setind  9165  hashfun  13788  hashf1lem2  13804  iswrdi  13855  ffz0iswrd  13881  dvdsrval  19326  thlle  20771  konigsberg  27964  hatomistici  30067  esumrnmpt2  31227  mppsval  32717  setindtr  39501  fourierdlem72  42344  afvpcfv0  43226
  Copyright terms: Public domain W3C validator