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

Theorem necon2abid 2984
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 2978 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
41, 3bitr4id 290 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wne 2941
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 2942
This theorem is referenced by:  sossfld  6186  funeldmb  7356  fin23lem24  10317  isf32lem4  10351  sqgt0sr  11101  leltne  11303  xrleltne  13124  xrltne  13142  ge0nemnf  13152  xlt2add  13239  supxrbnd  13307  supxrre2  13310  ioopnfsup  13829  icopnfsup  13830  xblpnfps  23901  xblpnf  23902  nmoreltpnf  30022  nmopreltpnf  31122  elprneb  45739
  Copyright terms: Public domain W3C validator