Theorem necon1bi 2983

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 2956	. . 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 2955

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 2956

This theorem is used by:  necon4ai  2986  iotanul2  6506  fvbr0  6905  peano5  7890  1stnpr  7990  2ndnpr  7991  1st2val  8014  2nd2val  8015  eceqoveq  8822  mapprc  8830  ixp0  8938  cnvfi  9170  setind  9726  hashfun  14502  hashf1lem2  14521  iswrdi  14582  ffz0iswrd  14606  dvdsrval  20502  thlle  21910  konigsberg  30737  hatomistici  32843  esumrnmpt2  34578  setindregs  35656  mppsval  36151  grpods  43060  unitscyglem4  43064  setindtr  43865  fourierdlem72  47006  afvpcfv0  48034