Theorem necon2abid 2967

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  sossfld  6139  funeldmb  7300  fin23lem24  10235  isf32lem4  10269  sqgt0sr  11019  leltne  11223  xrleltne  13065  xrltne  13083  ge0nemnf  13093  xlt2add  13180  supxrbnd  13248  supxrre2  13251  ioopnfsup  13786  icopnfsup  13787  xblpnfps  24299  xblpnf  24300  nmoreltpnf  30731  nmopreltpnf  31831  elprneb  47014