Theorem necon1bi 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 2935

This theorem is referenced by:  necon4ai  2965  iotanul2  6458  fvbr0  6854  peano5  7833  1stnpr  7935  2ndnpr  7936  1st2val  7959  2nd2val  7960  eceqoveq  8759  mapprc  8767  ixp0  8869  cnvfi  9100  setind  9659  hashfun  14390  hashf1lem2  14409  iswrdi  14470  ffz0iswrd  14494  dvdsrval  20332  thlle  21672  konigsberg  30345  hatomistici  32451  esumrnmpt2  34252  setindregs  35311  mppsval  35800  grpods  42679  unitscyglem4  42683  setindtr  43469  fourierdlem72  46621  afvpcfv0  47609