Theorem necon1bi 2956

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 2929	. . 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 2928

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 2929

This theorem is referenced by:  necon4ai  2959  iotanul2  6449  fvbr0  6844  peano5  7818  1stnpr  7920  2ndnpr  7921  1st2val  7944  2nd2val  7945  eceqoveq  8741  mapprc  8749  ixp0  8850  cnvfi  9080  setind  9632  hashfun  14339  hashf1lem2  14358  iswrdi  14419  ffz0iswrd  14443  dvdsrval  20274  thlle  21629  konigsberg  30229  hatomistici  32334  esumrnmpt2  34073  setindregs  35120  mppsval  35608  grpods  42227  unitscyglem4  42231  setindtr  43057  fourierdlem72  46216  afvpcfv0  47177