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  6793  peano5  7730  peano5OLD  7731  1stnpr  7824  2ndnpr  7825  1st2val  7848  2nd2val  7849  eceqoveq  8598  mapprc  8606  ixp0  8706  cnvfi  8950  setind  9501  hashfun  14162  hashf1lem2  14180  iswrdi  14231  ffz0iswrd  14254  dvdsrval  19897  thlle  20913  thlleOLD  20914  konigsberg  28629  hatomistici  30732  esumrnmpt2  32044  mppsval  33542  sn-iotanul  40202  setindtr  40854  fourierdlem72  43700  afvpcfv0  44616