Theorem necon1bi 2959

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

Step	Hyp	Ref	Expression
1		df-ne 2932	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bi.1	. . 3 ⊢ (𝐴 ≠ 𝐵 → 𝜑)
3	1, 2	sylbir 235	. 2 ⊢ (¬ 𝐴 = 𝐵 → 𝜑)
4	3	con1i 147	1 ⊢ (¬ 𝜑 → 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2931

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 207  df-ne 2932

This theorem is referenced by:  necon4ai  2962  iotanul2  6512  fvbr0  6916  peano5  7898  1stnpr  8001  2ndnpr  8002  1st2val  8025  2nd2val  8026  eceqoveq  8845  mapprc  8853  ixp0  8954  cnvfi  9199  setind  9757  hashfun  14459  hashf1lem2  14478  iswrdi  14539  ffz0iswrd  14562  dvdsrval  20334  thlle  21683  thlleOLD  21684  konigsberg  30223  hatomistici  32328  esumrnmpt2  34010  mppsval  35518  grpods  42136  unitscyglem4  42140  setindtr  42981  fourierdlem72  46138  afvpcfv0  47104