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 1570   ≠ 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  8169  omwordi  8558  omass  8567  nnmwordi  8623  pceq0  16963  f1otrspeq  19574  pmtrfinv  19588  symggen  19597  psgnunilem1  19620  mdetralt  22830  mdetunilem7  22840  ftalem5  27313  fsumvma  27449  dchrelbas4  27479  nosepssdm  27922  creq0  33207  suppgsumssiun  33512  fsumcvg4  34460  lkreqN  40043  flt4lem5elem  43497