Theorem necon1bi 2972

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon4ai  2975  fvbr0  6801  peano5  7740  peano5OLD  7741  1stnpr  7835  2ndnpr  7836  1st2val  7859  2nd2val  7860  eceqoveq  8611  mapprc  8619  ixp0  8719  cnvfi  8963  setind  9492  hashfun  14152  hashf1lem2  14170  iswrdi  14221  ffz0iswrd  14244  dvdsrval  19887  thlle  20903  thlleOLD  20904  konigsberg  28621  hatomistici  30724  esumrnmpt2  32036  mppsval  33534  sn-iotanul  40194  setindtr  40846  fourierdlem72  43719  afvpcfv0  44638