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 205   = wceq 1542  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 206  df-ne 2941
This theorem is referenced by:  sossfld  6139  funeldmb  7305  fin23lem24  10263  isf32lem4  10297  sqgt0sr  11047  leltne  11249  xrleltne  13070  xrltne  13088  ge0nemnf  13098  xlt2add  13185  supxrbnd  13253  supxrre2  13256  ioopnfsup  13775  icopnfsup  13776  xblpnfps  23764  xblpnf  23765  nmoreltpnf  29753  nmopreltpnf  30853  elprneb  45349
  Copyright terms: Public domain W3C validator