Theorem necon2abid 3003

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

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

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 2962

This theorem is used by:  sossfld  6189  funeldmb  7370  fin23lem24  10324  isf32lem4  10358  sqgt0sr  11109  leltne  11317  xrleltne  13188  xrltne  13206  ge0nemnf  13217  xlt2add  13304  supxrbnd  13372  supxrre2  13375  ioopnfsup  13917  icopnfsup  13918  xblpnfps  24589  xblpnf  24590  nmoreltpnf  31158  nmopreltpnf  32258  mh-inf3f1  37093  elprneb  47807