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 1542   ≠ 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  6471  fvbr0  6867  peano5  7844  1stnpr  7946  2ndnpr  7947  1st2val  7970  2nd2val  7971  eceqoveq  8769  mapprc  8777  ixp0  8879  cnvfi  9110  setind  9668  hashfun  14399  hashf1lem2  14418  iswrdi  14479  ffz0iswrd  14503  dvdsrval  20341  thlle  21677  konigsberg  30327  hatomistici  32433  esumrnmpt2  34212  setindregs  35274  mppsval  35754  grpods  42633  unitscyglem4  42637  setindtr  43452  fourierdlem72  46606  afvpcfv0  47594