Theorem necon1bi 2851

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon4ai  2854  fvbr0  6253  peano5  7131  1stnpr  7214  2ndnpr  7215  1st2val  7238  2nd2val  7239  eceqoveq  7895  mapprc  7903  ixp0  7983  setind  8648  hashfun  13262  hashf1lem2  13278  iswrdi  13341  dvdsrval  18691  thlle  20089  konigsberg  27235  hatomistici  29349  esumrnmpt2  30258  mppsval  31595  setindtr  37908  fourierdlem72  40713  afvpcfv0  41547