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

Theorem necon2abid 3056
 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 necon2abid.1 . . 3 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
21necon3abid 3050 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
3 notnotb 318 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
42, 3syl6rbbr 293 1 (𝜑 → (𝜓𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 3014 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 210  df-ne 3015 This theorem is referenced by:  sossfld  6030  fin23lem24  9736  isf32lem4  9770  sqgt0sr  10520  leltne  10722  xrleltne  12531  xrltne  12549  ge0nemnf  12559  xlt2add  12646  supxrbnd  12714  supxrre2  12717  ioopnfsup  13232  icopnfsup  13233  xblpnfps  22998  xblpnf  22999  nmoreltpnf  28548  nmopreltpnf  29648  funeldmb  33031  elprneb  43484
 Copyright terms: Public domain W3C validator