Theorem necon1bi 2810

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon4ai  2813  fvbr0  6125  peano5  6981  1stnpr  7063  2ndnpr  7064  1st2val  7085  2nd2val  7086  eceqoveq  7740  mapprc  7748  ixp0  7827  setind  8493  hashfun  13084  hashf1lem2  13097  iswrdi  13164  dvdsrval  18468  thlle  19860  konigsberg  26514  hatomistici  28605  esumrnmpt2  29457  mppsval  30723  setindtr  36609  fourierdlem72  39071  afvpcfv0  39875  konigsberg-av  41427