Theorem necon1bi 2963

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 2935	. . 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 2934

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 2935

This theorem is referenced by:  necon4ai  2966  iotanul2  6507  fvbr0  6914  peano5  7881  peano5OLD  7882  1stnpr  7978  2ndnpr  7979  1st2val  8002  2nd2val  8003  eceqoveq  8818  mapprc  8826  ixp0  8927  cnvfi  9182  setind  9731  hashfun  14402  hashf1lem2  14423  iswrdi  14474  ffz0iswrd  14497  dvdsrval  20263  thlle  21591  thlleOLD  21592  konigsberg  30019  hatomistici  32124  esumrnmpt2  33596  mppsval  35091  setindtr  42341  fourierdlem72  45466  afvpcfv0  46426