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

Theorem necon4bd 2798
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 2794 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 123 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 34 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2776
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 195  df-ne 2778
This theorem is referenced by:  om00  7516  pw2f1olem  7923  xlt2add  11916  hashfun  13033  hashtpg  13068  fsumcl2lem  14252  fprodcl2lem  14462  gcdeq0  15019  lcmeq0  15094  lcmfeq0b  15124  phibndlem  15256  abvn0b  19066  cfinufil  21481  isxmet2d  21880  i1fres  23192  tdeglem4  23538  ply1domn  23601  pilem2  23924  isnsqf  24575  ppieq0  24616  chpeq0  24647  chteq0  24648  ltrnatlw  34288  bcc0  37361
  Copyright terms: Public domain W3C validator