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

Theorem necon4bd 2989
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 2985 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 128 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1601  wne 2969
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 2970
This theorem is referenced by:  om00  7939  pw2f1olem  8352  xlt2add  12402  hashfun  13538  hashtpg  13581  fsumcl2lem  14869  fprodcl2lem  15083  gcdeq0  15644  lcmeq0  15719  lcmfeq0b  15749  phibndlem  15879  abvn0b  19699  cfinufil  22140  isxmet2d  22540  i1fres  23909  tdeglem4  24257  ply1domn  24320  pilem2  24643  isnsqf  25313  ppieq0  25354  chpeq0  25385  chteq0  25386  ltrnatlw  36337  bcc0  39495
  Copyright terms: Public domain W3C validator