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

Theorem necon2abid 3014
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 3008 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
3 notnotb 307 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
42, 3syl6rbbr 282 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198   = wceq 1653  wne 2972
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 199  df-ne 2973
This theorem is referenced by:  sossfld  5798  fin23lem24  9433  isf32lem4  9467  sqgt0sr  10216  leltne  10418  xrleltne  12224  xrltne  12242  ge0nemnf  12252  xlt2add  12338  supxrbnd  12406  supxrre2  12409  ioopnfsup  12917  icopnfsup  12918  xblpnfps  22527  xblpnf  22528  nmoreltpnf  28148  nmopreltpnf  29252  funeldmb  32174  elprneb  41912
  Copyright terms: Public domain W3C validator