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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ 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 206  df-ne 2933

This theorem is referenced by:  necon4ai  2964  iotanul2  6503  fvbr0  6910  peano5  7877  peano5OLD  7878  1stnpr  7972  2ndnpr  7973  1st2val  7996  2nd2val  7997  eceqoveq  8811  mapprc  8819  ixp0  8920  cnvfi  9175  setind  9724  hashfun  14393  hashf1lem2  14413  iswrdi  14464  ffz0iswrd  14487  dvdsrval  20248  thlle  21551  thlleOLD  21552  konigsberg  29934  hatomistici  32039  esumrnmpt2  33521  mppsval  35018  setindtr  42218  fourierdlem72  45345  afvpcfv0  46305