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 1569   ≠ 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  6511  fvbr0  6913  peano5  7906  1stnpr  8006  2ndnpr  8007  1st2val  8030  2nd2val  8031  eceqoveq  8847  mapprc  8855  ixp0  8963  cnvfi  9195  setind  9752  hashfun  14586  hashf1lem2  14605  iswrdi  14666  ffz0iswrd  14690  dvdsrval  20597  thlle  22009  konigsberg  30864  hatomistici  32970  esumrnmpt2  34747  setindregs  35855  mppsval  36424  grpods  43338  unitscyglem4  43342  setindtr  44125  fourierdlem72  47282  afvpcfv0  48310