Theorem necon1bi 2987

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  necon4ai  2990  iotanul2  6537  fvbr0  6943  peano5  7939  1stnpr  8039  2ndnpr  8040  1st2val  8063  2nd2val  8064  eceqoveq  8881  mapprc  8889  ixp0  8997  cnvfi  9229  setind  9785  hashfun  14623  hashf1lem2  14642  iswrdi  14703  ffz0iswrd  14727  dvdsrval  20642  thlle  22058  konigsberg  30915  hatomistici  33021  esumrnmpt2  34811  setindregs  35939  mppsval  36545  grpods  43510  unitscyglem4  43514  setindtr  44297  fourierdlem72  47461  afvpcfv0  48489