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

Theorem necon4bd 2810
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon4bd.1 (𝜑 → (¬ 𝜓𝐴𝐵))
Assertion
Ref Expression
necon4bd (𝜑 → (𝐴 = 𝐵𝜓))

Proof of Theorem necon4bd
StepHypRef Expression
1 necon4bd.1 . . 3 (𝜑 → (¬ 𝜓𝐴𝐵))
21necon2bd 2806 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 125 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wne 2790
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 197  df-ne 2791
This theorem is referenced by:  om00  7615  pw2f1olem  8024  xlt2add  12049  hashfun  13180  hashtpg  13221  fsumcl2lem  14411  fprodcl2lem  14624  gcdeq0  15181  lcmeq0  15256  lcmfeq0b  15286  phibndlem  15418  abvn0b  19242  cfinufil  21672  isxmet2d  22072  i1fres  23412  tdeglem4  23758  ply1domn  23821  pilem2  24144  isnsqf  24795  ppieq0  24836  chpeq0  24867  chteq0  24868  ltrnatlw  34989  bcc0  38060
  Copyright terms: Public domain W3C validator