Theorem necon1bi 2968

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 2940	. . 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 2939

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 2940

This theorem is referenced by:  necon4ai  2971  iotanul2  6471  fvbr0  6876  peano5  7835  peano5OLD  7836  1stnpr  7930  2ndnpr  7931  1st2val  7954  2nd2val  7955  eceqoveq  8768  mapprc  8776  ixp0  8876  cnvfi  9131  setind  9679  hashfun  14347  hashf1lem2  14367  iswrdi  14418  ffz0iswrd  14441  dvdsrval  20088  thlle  21139  thlleOLD  21140  konigsberg  29264  hatomistici  31367  esumrnmpt2  32756  mppsval  34253  setindtr  41406  fourierdlem72  44539  afvpcfv0  45498