Theorem necon1bi 2986

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon4ai  2989  iotanul2  6511  fvbr0  6910  peano5  7891  1stnpr  7991  2ndnpr  7992  1st2val  8015  2nd2val  8016  eceqoveq  8821  mapprc  8829  ixp0  8930  cnvfi  9161  setind  9717  hashfun  14476  hashf1lem2  14495  iswrdi  14556  ffz0iswrd  14580  dvdsrval  20444  thlle  21828  konigsberg  30589  hatomistici  32695  esumrnmpt2  34439  setindregs  35524  mppsval  36045  grpods  42942  unitscyglem4  42946  setindtr  43734  fourierdlem72  46875  afvpcfv0  47866