Theorem necon1bi 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 2941

This theorem is referenced by:  necon4ai  2972  iotanul2  6513  fvbr0  6920  peano5  7886  peano5OLD  7887  1stnpr  7981  2ndnpr  7982  1st2val  8005  2nd2val  8006  eceqoveq  8818  mapprc  8826  ixp0  8927  cnvfi  9182  setind  9731  hashfun  14399  hashf1lem2  14419  iswrdi  14470  ffz0iswrd  14493  dvdsrval  20179  thlle  21257  thlleOLD  21258  konigsberg  29548  hatomistici  31653  esumrnmpt2  33135  mppsval  34632  setindtr  41845  fourierdlem72  44973  afvpcfv0  45933