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

Theorem necon2abid 2833
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 2827 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
3 notnotb 304 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
42, 3syl6rbbr 279 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1481  wne 2791
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 197  df-ne 2792
This theorem is referenced by:  sossfld  5568  fin23lem24  9129  isf32lem4  9163  sqgt0sr  9912  leltne  10112  xrleltne  11963  xrltne  11979  ge0nemnf  11989  xlt2add  12075  supxrbnd  12143  supxrre2  12146  ioopnfsup  12646  icopnfsup  12647  xblpnfps  22181  xblpnf  22182  nmoreltpnf  27594  nmopreltpnf  28698  funeldmb  31637  elprneb  41059
  Copyright terms: Public domain W3C validator