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

Theorem necon2abid 2819
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 2813 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
3 notnotb 302 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
42, 3syl6rbbr 277 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194   = wceq 1474  wne 2775
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 195  df-ne 2777
This theorem is referenced by:  sossfld  5481  fin23lem24  9000  isf32lem4  9034  sqgt0sr  9779  leltne  9974  xrleltne  11809  xrltne  11825  ge0nemnf  11833  xlt2add  11915  supxrbnd  11982  supxrre2  11985  ioopnfsup  12476  icopnfsup  12477  xblpnfps  21947  xblpnf  21948  nmoreltpnf  26810  nmopreltpnf  27914  elprneb  39740
  Copyright terms: Public domain W3C validator