Theorem necon1bi 2967

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon4ai  2970  iotanul2  6533  fvbr0  6936  peano5  7916  1stnpr  8017  2ndnpr  8018  1st2val  8041  2nd2val  8042  eceqoveq  8861  mapprc  8869  ixp0  8970  cnvfi  9215  setind  9772  hashfun  14473  hashf1lem2  14492  iswrdi  14553  ffz0iswrd  14576  dvdsrval  20378  thlle  21734  thlleOLD  21735  konigsberg  30286  hatomistici  32391  esumrnmpt2  34049  mppsval  35557  grpods  42176  unitscyglem4  42180  setindtr  43013  fourierdlem72  46134  afvpcfv0  47096