Theorem necon1bi 2992

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 2965

This theorem is referenced by:  necon4ai  2995  iotanul2  6506  fvbr0  6906  peano5  7886  1stnpr  7986  2ndnpr  7987  1st2val  8010  2nd2val  8011  eceqoveq  8816  mapprc  8824  ixp0  8925  cnvfi  9156  setind  9712  hashfun  14470  hashf1lem2  14489  iswrdi  14550  ffz0iswrd  14574  dvdsrval  20439  thlle  21812  konigsberg  30545  hatomistici  32651  esumrnmpt2  34399  setindregs  35462  mppsval  35959  grpods  42846  unitscyglem4  42850  setindtr  43636  fourierdlem72  46777  afvpcfv0  47765