Theorem necon1bi 2971

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  necon4ai  2974  fvbr0  6783  peano5  7714  peano5OLD  7715  1stnpr  7808  2ndnpr  7809  1st2val  7832  2nd2val  7833  eceqoveq  8569  mapprc  8577  ixp0  8677  cnvfi  8924  setind  9423  hashfun  14080  hashf1lem2  14098  iswrdi  14149  ffz0iswrd  14172  dvdsrval  19802  thlle  20814  konigsberg  28522  hatomistici  30625  esumrnmpt2  31936  mppsval  33434  sn-iotanul  40121  setindtr  40762  fourierdlem72  43609  afvpcfv0  44525