Theorem necon2abid 2997

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

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

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 2956

This theorem is used by:  sossfld  6177  funeldmb  7369  fin23lem24  10403  isf32lem4  10437  sqgt0sr  11194  leltne  11402  xrleltne  13277  xrltne  13295  ge0nemnf  13306  xlt2add  13393  supxrbnd  13461  supxrre2  13464  ioopnfsup  14007  icopnfsup  14008  xblpnfps  24719  xblpnf  24720  nmoreltpnf  31376  nmopreltpnf  32476  elprneb  48192