Theorem necon1bi 3015

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necon4ai  3018  fvbr0  6672  peano5  7585  1stnpr  7675  2ndnpr  7676  1st2val  7699  2nd2val  7700  eceqoveq  8385  mapprc  8393  ixp0  8478  setind  9160  hashfun  13794  hashf1lem2  13810  iswrdi  13861  ffz0iswrd  13884  dvdsrval  19391  thlle  20386  konigsberg  28042  hatomistici  30145  esumrnmpt2  31437  mppsval  32932  setindtr  39965  fourierdlem72  42820  afvpcfv0  43702