Theorem necon1bi 2961

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

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

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 207  df-ne 2934

This theorem is referenced by:  necon4ai  2964  iotanul2  6473  fvbr0  6869  peano5  7845  1stnpr  7947  2ndnpr  7948  1st2val  7971  2nd2val  7972  eceqoveq  8771  mapprc  8779  ixp0  8881  cnvfi  9112  setind  9668  hashfun  14372  hashf1lem2  14391  iswrdi  14452  ffz0iswrd  14476  dvdsrval  20309  thlle  21664  konigsberg  30344  hatomistici  32449  esumrnmpt2  34245  setindregs  35305  mppsval  35785  grpods  42561  unitscyglem4  42565  setindtr  43378  fourierdlem72  46533  afvpcfv0  47503