Theorem necon1bi 2960

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necon4ai  2963  iotanul2  6465  fvbr0  6861  peano5  7835  1stnpr  7937  2ndnpr  7938  1st2val  7961  2nd2val  7962  eceqoveq  8759  mapprc  8767  ixp0  8869  cnvfi  9100  setind  9656  hashfun  14360  hashf1lem2  14379  iswrdi  14440  ffz0iswrd  14464  dvdsrval  20297  thlle  21652  konigsberg  30332  hatomistici  32437  esumrnmpt2  34225  setindregs  35286  mppsval  35766  grpods  42448  unitscyglem4  42452  setindtr  43266  fourierdlem72  46422  afvpcfv0  47392