Theorem necon2abid 3002

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		notnotb 318	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		necon2abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
3	2	necon3abid 2996	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
4	1, 3	bitr4id 293	1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  sossfld  6176  funeldmb  7347  fin23lem24  10294  isf32lem4  10328  sqgt0sr  11079  leltne  11287  xrleltne  13161  xrltne  13179  ge0nemnf  13190  xlt2add  13277  supxrbnd  13345  supxrre2  13348  ioopnfsup  13888  icopnfsup  13889  xblpnfps  24513  xblpnf  24514  nmoreltpnf  31030  nmopreltpnf  32130  mh-inf3f1  36914  elprneb  47621