Theorem necon2bbid 2984

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 2981	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

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

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 2941

This theorem is referenced by:  necon4bid  2986  omwordi  8570  omass  8579  nnmwordi  8634  sdom1OLD  9242  pceq0  16803  f1otrspeq  19314  pmtrfinv  19328  symggen  19337  psgnunilem1  19360  mdetralt  22109  mdetunilem7  22119  ftalem5  26578  fsumvma  26713  dchrelbas4  26743  nosepssdm  27186  fvdifsupp  31902  creq0  31955  fsumcvg4  32925  lkreqN  38035  flt4lem5elem  41394