Theorem necon2abid 2824

Description: Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)

Hypothesis

Ref	Expression
necon2abid.1	⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

Assertion

Ref	Expression
necon2abid	⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Proof of Theorem necon2abid

Step	Hyp	Ref	Expression
1		necon2abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
2	1	necon3abid 2818	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
3		notnotb 303	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
4	2, 3	syl6rbbr 278	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:  sossfld  5499  fin23lem24  9027  isf32lem4  9061  sqgt0sr  9806  leltne  10006  xrleltne  11854  xrltne  11870  ge0nemnf  11878  xlt2add  11962  supxrbnd  12030  supxrre2  12033  ioopnfsup  12525  icopnfsup  12526  xblpnfps  22010  xblpnf  22011  nmoreltpnf  27008  nmopreltpnf  28112  elprneb  39939