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  6466  fvbr0  6862  peano5  7837  1stnpr  7939  2ndnpr  7940  1st2val  7963  2nd2val  7964  eceqoveq  8763  mapprc  8771  ixp0  8873  cnvfi  9104  setind  9660  hashfun  14364  hashf1lem2  14383  iswrdi  14444  ffz0iswrd  14468  dvdsrval  20301  thlle  21656  konigsberg  30315  hatomistici  32420  esumrnmpt2  34206  setindregs  35267  mppsval  35747  grpods  42485  unitscyglem4  42489  setindtr  43302  fourierdlem72  46458  afvpcfv0  47428