Theorem necon2abid 3058

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		necon2abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
2	1	necon3abid 3052	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
3		notnotb 317	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
4	2, 3	syl6rbbr 292	1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  sossfld  6043  fin23lem24  9744  isf32lem4  9778  sqgt0sr  10528  leltne  10730  xrleltne  12539  xrltne  12557  ge0nemnf  12567  xlt2add  12654  supxrbnd  12722  supxrre2  12725  ioopnfsup  13233  icopnfsup  13234  xblpnfps  23005  xblpnf  23006  nmoreltpnf  28546  nmopreltpnf  29646  funeldmb  33006  elprneb  43284