Theorem necon1bi 2953

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 2926	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bi.1	. . 3 ⊢ (𝐴 ≠ 𝐵 → 𝜑)
3	1, 2	sylbir 235	. 2 ⊢ (¬ 𝐴 = 𝐵 → 𝜑)
4	3	con1i 147	1 ⊢ (¬ 𝜑 → 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon4ai  2956  iotanul2  6481  fvbr0  6887  peano5  7869  1stnpr  7972  2ndnpr  7973  1st2val  7996  2nd2val  7997  eceqoveq  8795  mapprc  8803  ixp0  8904  cnvfi  9140  setind  9687  hashfun  14402  hashf1lem2  14421  iswrdi  14482  ffz0iswrd  14506  dvdsrval  20270  thlle  21606  konigsberg  30186  hatomistici  32291  esumrnmpt2  34058  mppsval  35559  grpods  42182  unitscyglem4  42186  setindtr  43013  fourierdlem72  46176  afvpcfv0  47147