Theorem necon2bbid 3003

Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)

Hypothesis

Ref	Expression
necon2bbid.1	⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Assertion

Ref	Expression
necon2bbid	⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon2bbid

Step	Hyp	Ref	Expression
1		necon2bbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))
2		notnotb 318	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3	1, 2	bitr3di 289	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
4	3	necon4abid 3000	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2960

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 2961

This theorem is used by:  necon4bid  3005  fvdifsupp  8169  omwordi  8558  omass  8567  nnmwordi  8623  pceq0  16948  f1otrspeq  19540  pmtrfinv  19554  symggen  19563  psgnunilem1  19586  mdetralt  22794  mdetunilem7  22804  ftalem5  27270  fsumvma  27406  dchrelbas4  27436  nosepssdm  27879  creq0  33110  suppgsumssiun  33415  fsumcvg4  34363  lkreqN  39977  flt4lem5elem  43416