Theorem necon1bi 2975

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon4ai  2978  iotanul2  6543  fvbr0  6949  peano5  7932  peano5OLD  7933  1stnpr  8034  2ndnpr  8035  1st2val  8058  2nd2val  8059  eceqoveq  8880  mapprc  8888  ixp0  8989  cnvfi  9243  setind  9803  hashfun  14486  hashf1lem2  14505  iswrdi  14566  ffz0iswrd  14589  dvdsrval  20387  thlle  21739  thlleOLD  21740  konigsberg  30289  hatomistici  32394  esumrnmpt2  34032  mppsval  35540  grpods  42151  unitscyglem4  42155  setindtr  42981  fourierdlem72  46099  afvpcfv0  47061