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

Theorem necon2abid 2981
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 2975 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
41, 3bitr4id 290 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1537  wne 2938
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 2939
This theorem is referenced by:  sossfld  6208  funeldmb  7379  fin23lem24  10360  isf32lem4  10394  sqgt0sr  11144  leltne  11348  xrleltne  13184  xrltne  13202  ge0nemnf  13212  xlt2add  13299  supxrbnd  13367  supxrre2  13370  ioopnfsup  13901  icopnfsup  13902  xblpnfps  24421  xblpnf  24422  nmoreltpnf  30798  nmopreltpnf  31898  elprneb  46979
  Copyright terms: Public domain W3C validator