Theorem necon1bi 2966

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2937

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 2938

This theorem is referenced by:  necon4ai  2969  iotanul2  6523  fvbr0  6931  peano5  7907  peano5OLD  7908  1stnpr  8005  2ndnpr  8006  1st2val  8029  2nd2val  8030  eceqoveq  8849  mapprc  8857  ixp0  8958  cnvfi  9213  setind  9767  hashfun  14438  hashf1lem2  14459  iswrdi  14510  ffz0iswrd  14533  dvdsrval  20314  thlle  21644  thlleOLD  21645  konigsberg  30095  hatomistici  32200  esumrnmpt2  33728  mppsval  35223  setindtr  42494  fourierdlem72  45613  afvpcfv0  46573