Theorem necon2abid 3014

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 3008	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ ¬ 𝜓))
3		notnotb 307	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
4	2, 3	syl6rbbr 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   = wceq 1653   ≠ wne 2972

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 199  df-ne 2973

This theorem is referenced by:  sossfld  5798  fin23lem24  9433  isf32lem4  9467  sqgt0sr  10216  leltne  10418  xrleltne  12224  xrltne  12242  ge0nemnf  12252  xlt2add  12338  supxrbnd  12406  supxrre2  12409  ioopnfsup  12917  icopnfsup  12918  xblpnfps  22527  xblpnf  22528  nmoreltpnf  28148  nmopreltpnf  29252  funeldmb  32174  elprneb  41912