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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1543   ≠ 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 210  df-ne 2941

This theorem is referenced by:  necon4bid  2986  omwordi  8299  omass  8308  nnmwordi  8363  sdom1  8878  pceq0  16424  f1otrspeq  18839  pmtrfinv  18853  symggen  18862  psgnunilem1  18885  mdetralt  21505  mdetunilem7  21515  ftalem5  25959  fsumvma  26094  dchrelbas4  26124  fvdifsupp  30738  creq0  30790  fsumcvg4  31614  nosepssdm  33626  lkreqN  36921  flt4lem5elem  40191