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

Theorem necon4bd 2960
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 2956 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 130 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  iftrueb  4538  om00  8613  pw2f1olem  9116  xlt2add  13302  hashfun  14476  hashtpg  14524  fsumcl2lem  15767  fprodcl2lem  15986  gcdeq0  16554  lcmeq0  16637  lcmfeq0b  16667  phibndlem  16807  abvn0b  20837  cfinufil  23936  isxmet2d  24337  i1fres  25740  tdeglem4  26099  ply1domn  26163  pilem2  26496  isnsqf  27178  ppieq0  27219  chpeq0  27252  chteq0  27253  ltrnatlw  40185  bcc0  44359
  Copyright terms: Public domain W3C validator