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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon4ai  2964  iotanul2  6465  fvbr0  6861  peano5  7837  1stnpr  7939  2ndnpr  7940  1st2val  7963  2nd2val  7964  eceqoveq  8762  mapprc  8770  ixp0  8872  cnvfi  9103  setind  9659  hashfun  14390  hashf1lem2  14409  iswrdi  14470  ffz0iswrd  14494  dvdsrval  20332  thlle  21687  konigsberg  30342  hatomistici  32448  esumrnmpt2  34228  setindregs  35290  mppsval  35770  grpods  42647  unitscyglem4  42651  setindtr  43470  fourierdlem72  46624  afvpcfv0  47606