Theorem necon1bi 3044

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

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

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 209  df-ne 3017

This theorem is referenced by:  necon4ai  3047  fvbr0  6697  peano5  7605  1stnpr  7693  2ndnpr  7694  1st2val  7717  2nd2val  7718  eceqoveq  8402  mapprc  8410  ixp0  8495  setind  9176  hashfun  13799  hashf1lem2  13815  iswrdi  13866  ffz0iswrd  13891  dvdsrval  19395  thlle  20841  konigsberg  28036  hatomistici  30139  esumrnmpt2  31327  mppsval  32819  setindtr  39641  fourierdlem72  42483  afvpcfv0  43365