Theorem necon2abid 3058

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  sossfld  6038  fin23lem24  9738  isf32lem4  9772  sqgt0sr  10522  leltne  10724  xrleltne  12532  xrltne  12550  ge0nemnf  12560  xlt2add  12647  supxrbnd  12715  supxrre2  12718  ioopnfsup  13226  icopnfsup  13227  xblpnfps  22999  xblpnf  23000  nmoreltpnf  28540  nmopreltpnf  29640  funeldmb  33001  elprneb  43257