Theorem necon1bi 2985

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 2958	. . 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 2957

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 2958

This theorem is used by:  necon4ai  2988  iotanul2  6510  fvbr0  6909  peano5  7894  1stnpr  7994  2ndnpr  7995  1st2val  8018  2nd2val  8019  eceqoveq  8826  mapprc  8834  ixp0  8942  cnvfi  9174  setind  9730  hashfun  14506  hashf1lem2  14525  iswrdi  14586  ffz0iswrd  14610  dvdsrval  20508  thlle  21916  konigsberg  30745  hatomistici  32851  esumrnmpt2  34586  setindregs  35664  mppsval  36159  grpods  43068  unitscyglem4  43072  setindtr  43873  fourierdlem72  47014  afvpcfv0  48042