Theorem necon1bi 2984

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 2957

This theorem is referenced by:  necon4ai  2987  iotanul2  6489  fvbr0  6889  peano5  7869  1stnpr  7969  2ndnpr  7970  1st2val  7993  2nd2val  7994  eceqoveq  8798  mapprc  8806  ixp0  8907  cnvfi  9138  setind  9696  hashfun  14444  hashf1lem2  14463  iswrdi  14524  ffz0iswrd  14548  dvdsrval  20397  thlle  21737  konigsberg  30416  hatomistici  32522  esumrnmpt2  34326  setindregs  35387  mppsval  35883  grpods  42772  unitscyglem4  42776  setindtr  43562  fourierdlem72  46713  afvpcfv0  47701