Theorem necon2bbid 3061

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon4bid  3063  omwordi  8199  omass  8208  nnmwordi  8263  sdom1  8720  pceq0  16209  f1otrspeq  18577  pmtrfinv  18591  symggen  18600  psgnunilem1  18623  mdetralt  21219  mdetunilem7  21229  ftalem5  25656  fsumvma  25791  dchrelbas4  25821  fvdifsupp  30429  creq0  30473  fsumcvg4  31195  nosepssdm  33192  lkreqN  36308