Theorem necon2bbid 2998

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon4bid  3000  fvdifsupp  8192  omwordi  8583  omass  8592  nnmwordi  8648  pceq0  17055  f1otrspeq  19667  pmtrfinv  19681  symggen  19690  psgnunilem1  19713  mdetralt  22929  mdetunilem7  22939  ftalem5  27410  fsumvma  27546  dchrelbas4  27576  flt4lem5elem  27987  nosepssdm  28049  creq0  33375  suppgsumssiun  33680  fsumcvg4  34629  lkreqN  40321