Theorem necon1bi 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon4ai  2956  iotanul2  6459  fvbr0  6853  peano5  7833  1stnpr  7935  2ndnpr  7936  1st2val  7959  2nd2val  7960  eceqoveq  8756  mapprc  8764  ixp0  8865  cnvfi  9100  setind  9649  hashfun  14362  hashf1lem2  14381  iswrdi  14442  ffz0iswrd  14466  dvdsrval  20264  thlle  21622  konigsberg  30219  hatomistici  32324  esumrnmpt2  34037  setindregs  35067  mppsval  35547  grpods  42170  unitscyglem4  42174  setindtr  43000  fourierdlem72  46163  afvpcfv0  47134