Theorem necon1bi 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon4ai  2960  iotanul2  6462  fvbr0  6858  peano5  7832  1stnpr  7934  2ndnpr  7935  1st2val  7958  2nd2val  7959  eceqoveq  8755  mapprc  8763  ixp0  8865  cnvfi  9096  setind  9648  hashfun  14351  hashf1lem2  14370  iswrdi  14431  ffz0iswrd  14455  dvdsrval  20288  thlle  21643  konigsberg  30258  hatomistici  32363  esumrnmpt2  34153  setindregs  35200  mppsval  35688  grpods  42360  unitscyglem4  42364  setindtr  43181  fourierdlem72  46338  afvpcfv0  47308