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

Theorem necon4bd 3020
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 3016 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 128 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1658  wne 3000
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 3001
This theorem is referenced by:  om00  7923  pw2f1olem  8334  xlt2add  12379  hashfun  13514  hashtpg  13557  fsumcl2lem  14840  fprodcl2lem  15054  gcdeq0  15612  lcmeq0  15687  lcmfeq0b  15717  phibndlem  15847  abvn0b  19664  cfinufil  22103  isxmet2d  22503  i1fres  23872  tdeglem4  24220  ply1domn  24283  pilem2  24606  isnsqf  25275  ppieq0  25316  chpeq0  25347  chteq0  25348  ltrnatlw  36259  bcc0  39380
  Copyright terms: Public domain W3C validator