Theorem necon2bbid 2963

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		notnotb 304	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		necon2bbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))
3	1, 2	syl5rbbr 275	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
4	3	necon4abid 2960	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   = wceq 1620   ≠ wne 2920

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 197  df-ne 2921

This theorem is referenced by:  necon4bid  2965  omwordi  7808  omass  7817  nnmwordi  7872  sdom1  8313  pceq0  15748  f1otrspeq  18038  pmtrfinv  18052  symggen  18061  psgnunilem1  18084  mdetralt  20587  mdetunilem7  20597  ftalem5  24973  fsumvma  25108  dchrelbas4  25138  fsumcvg4  30276  nosepssdm  32113  lkreqN  34929