Theorem necon2bbid 2982

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ 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 206  df-ne 2939

This theorem is referenced by:  necon4bid  2984  omwordi  8573  omass  8582  nnmwordi  8637  sdom1OLD  9245  pceq0  16808  f1otrspeq  19356  pmtrfinv  19370  symggen  19379  psgnunilem1  19402  mdetralt  22330  mdetunilem7  22340  ftalem5  26817  fsumvma  26952  dchrelbas4  26982  nosepssdm  27425  fvdifsupp  32174  creq0  32227  fsumcvg4  33228  lkreqN  38343  flt4lem5elem  41695