Theorem necon2bbid 2987

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 315	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3	1, 2	bitr3di 286	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
4	3	necon4abid 2984	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon4bid  2989  omwordi  8402  omass  8411  nnmwordi  8466  sdom1  9022  pceq0  16572  f1otrspeq  19055  pmtrfinv  19069  symggen  19078  psgnunilem1  19101  mdetralt  21757  mdetunilem7  21767  ftalem5  26226  fsumvma  26361  dchrelbas4  26391  fvdifsupp  31018  creq0  31070  fsumcvg4  31900  nosepssdm  33889  lkreqN  37184  flt4lem5elem  40488