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

Theorem necon2abid 2983
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 notnotb 315 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2abid.1 . . 3 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
32necon3abid 2977 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
41, 3bitr4id 290 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1540  wne 2940
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 2941
This theorem is referenced by:  sossfld  6206  funeldmb  7379  fin23lem24  10362  isf32lem4  10396  sqgt0sr  11146  leltne  11350  xrleltne  13187  xrltne  13205  ge0nemnf  13215  xlt2add  13302  supxrbnd  13370  supxrre2  13373  ioopnfsup  13904  icopnfsup  13905  xblpnfps  24405  xblpnf  24406  nmoreltpnf  30788  nmopreltpnf  31888  elprneb  47041
  Copyright terms: Public domain W3C validator