Theorem necon1bi 2984

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon4ai  2987  iotanul2  6510  fvbr0  6910  peano5  7903  1stnpr  8003  2ndnpr  8004  1st2val  8027  2nd2val  8028  eceqoveq  8836  mapprc  8844  ixp0  8952  cnvfi  9184  setind  9741  hashfun  14575  hashf1lem2  14594  iswrdi  14655  ffz0iswrd  14679  dvdsrval  20584  thlle  21996  konigsberg  30851  hatomistici  32957  esumrnmpt2  34693  setindregs  35781  mppsval  36316  grpods  43224  unitscyglem4  43228  setindtr  44010  fourierdlem72  47157  afvpcfv0  48185