Theorem necon1bi 3042

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1531   ≠ wne 3014

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 209  df-ne 3015

This theorem is referenced by:  necon4ai  3045  fvbr0  6690  peano5  7597  1stnpr  7685  2ndnpr  7686  1st2val  7709  2nd2val  7710  eceqoveq  8394  mapprc  8402  ixp0  8487  setind  9168  hashfun  13790  hashf1lem2  13806  iswrdi  13857  ffz0iswrd  13883  dvdsrval  19387  thlle  20833  konigsberg  28028  hatomistici  30131  esumrnmpt2  31320  mppsval  32812  setindtr  39611  fourierdlem72  42453  afvpcfv0  43335