Theorem necon1bi 2970

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon4ai  2973  iotanul2  6514  fvbr0  6921  peano5  7884  peano5OLD  7885  1stnpr  7979  2ndnpr  7980  1st2val  8003  2nd2val  8004  eceqoveq  8816  mapprc  8824  ixp0  8925  cnvfi  9180  setind  9729  hashfun  14397  hashf1lem2  14417  iswrdi  14468  ffz0iswrd  14491  dvdsrval  20175  thlle  21251  thlleOLD  21252  konigsberg  29510  hatomistici  31615  esumrnmpt2  33066  mppsval  34563  setindtr  41763  fourierdlem72  44894  afvpcfv0  45854