Theorem necon2bbid 2825

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon4bid  2827  omwordi  7538  omass  7547  nnmwordi  7602  sdom1  8045  pceq0  15413  f1otrspeq  17690  pmtrfinv  17704  symggen  17713  psgnunilem1  17736  mdetralt  20233  mdetunilem7  20243  ftalem5  24603  fsumvma  24738  dchrelbas4  24768  fsumcvg4  29324  lkreqN  33475