Theorem necon2abid 2998

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 2992	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
4	1, 3	bitr4id 293	1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2956

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 2957

This theorem is used by:  sossfld  6177  funeldmb  7361  fin23lem24  10381  isf32lem4  10415  sqgt0sr  11172  leltne  11380  xrleltne  13255  xrltne  13273  ge0nemnf  13284  xlt2add  13371  supxrbnd  13439  supxrre2  13442  ioopnfsup  13984  icopnfsup  13985  xblpnfps  24694  xblpnf  24695  nmoreltpnf  31353  nmopreltpnf  32453  elprneb  48043