Theorem necon2abid 2836

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 2830	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
3		notnotb 304	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
4	2, 3	syl6rbbr 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  sossfld  5580  fin23lem24  9144  isf32lem4  9178  sqgt0sr  9927  leltne  10127  xrleltne  11978  xrltne  11994  ge0nemnf  12004  xlt2add  12090  supxrbnd  12158  supxrre2  12161  ioopnfsup  12663  icopnfsup  12664  xblpnfps  22200  xblpnf  22201  nmoreltpnf  27624  nmopreltpnf  28728  funeldmb  31661  elprneb  41296