Theorem necon1bi 2988

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 2961	. . 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 2960

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 2961

This theorem is used by:  necon4ai  2991  iotanul2  6513  fvbr0  6912  peano5  7892  1stnpr  7992  2ndnpr  7993  1st2val  8016  2nd2val  8017  eceqoveq  8822  mapprc  8830  ixp0  8931  cnvfi  9163  setind  9719  hashfun  14488  hashf1lem2  14507  iswrdi  14568  ffz0iswrd  14592  dvdsrval  20469  thlle  21877  konigsberg  30655  hatomistici  32761  esumrnmpt2  34498  setindregs  35576  mppsval  36077  grpods  42994  unitscyglem4  42998  setindtr  43784  fourierdlem72  46925  afvpcfv0  47916