MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2abid Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 necon2abid.1 . . 3 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
21necon3abid 3052 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
3 notnotb 316 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
42, 3syl6rbbr 291 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1528  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 208  df-ne 3017
This theorem is referenced by:  sossfld  6037  fin23lem24  9733  isf32lem4  9767  sqgt0sr  10517  leltne  10719  xrleltne  12528  xrltne  12546  ge0nemnf  12556  xlt2add  12643  supxrbnd  12711  supxrre2  12714  ioopnfsup  13222  icopnfsup  13223  xblpnfps  22934  xblpnf  22935  nmoreltpnf  28474  nmopreltpnf  29574  funeldmb  32904  elprneb  43145
  Copyright terms: Public domain W3C validator