Theorem necon1bi 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2933

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 2934

This theorem is referenced by:  necon4ai  2964  iotanul2  6506  fvbr0  6910  peano5  7894  1stnpr  7997  2ndnpr  7998  1st2val  8021  2nd2val  8022  eceqoveq  8841  mapprc  8849  ixp0  8950  cnvfi  9195  setind  9753  hashfun  14460  hashf1lem2  14479  iswrdi  14540  ffz0iswrd  14564  dvdsrval  20326  thlle  21662  konigsberg  30243  hatomistici  32348  esumrnmpt2  34104  mppsval  35599  grpods  42212  unitscyglem4  42216  setindtr  43023  fourierdlem72  46187  afvpcfv0  47155