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

Theorem necon2abid 2973
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 314 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2abid.1 . . 3 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
32necon3abid 2967 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
41, 3bitr4id 289 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1534  wne 2930
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 206  df-ne 2931
This theorem is referenced by:  sossfld  6197  funeldmb  7371  fin23lem24  10365  isf32lem4  10399  sqgt0sr  11149  leltne  11353  xrleltne  13178  xrltne  13196  ge0nemnf  13206  xlt2add  13293  supxrbnd  13361  supxrre2  13364  ioopnfsup  13884  icopnfsup  13885  xblpnfps  24392  xblpnf  24393  nmoreltpnf  30702  nmopreltpnf  31802  elprneb  46644
  Copyright terms: Public domain W3C validator