Theorem necon1bi 2822

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon4ai  2825  fvbr0  6215  peano5  7089  1stnpr  7172  2ndnpr  7173  1st2val  7194  2nd2val  7195  eceqoveq  7853  mapprc  7861  ixp0  7941  setind  8610  hashfun  13224  hashf1lem2  13240  iswrdi  13309  dvdsrval  18645  thlle  20041  konigsberg  27119  hatomistici  29221  esumrnmpt2  30130  mppsval  31469  setindtr  37591  fourierdlem72  40395  afvpcfv0  41226