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

Theorem necon4bd 2944
 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 2940 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 125 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1624   ≠ wne 2924 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 2925 This theorem is referenced by:  om00  7816  pw2f1olem  8221  xlt2add  12275  hashfun  13408  hashtpg  13451  fsumcl2lem  14653  fprodcl2lem  14871  gcdeq0  15432  lcmeq0  15507  lcmfeq0b  15537  phibndlem  15669  abvn0b  19496  cfinufil  21925  isxmet2d  22325  i1fres  23663  tdeglem4  24011  ply1domn  24074  pilem2  24397  isnsqf  25052  ppieq0  25093  chpeq0  25124  chteq0  25125  ltrnatlw  35965  bcc0  39033
 Copyright terms: Public domain W3C validator