Theorem necon2bbid 3002

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

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

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 2960

This theorem is used by:  necon4bid  3004  fvdifsupp  8226  omwordi  8617  omass  8626  nnmwordi  8682  pceq0  17093  f1otrspeq  19712  pmtrfinv  19726  symggen  19735  psgnunilem1  19758  mdetralt  22978  mdetunilem7  22988  ftalem5  27461  fsumvma  27597  dchrelbas4  27627  flt4lem5elem  28038  nosepssdm  28100  creq0  33424  suppgsumssiun  33732  fsumcvg4  34693  lkreqN  40493