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

Theorem necon4bd 3031
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 3027 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 132 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 3011
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 210  df-ne 3012
This theorem is referenced by:  om00  8188  pw2f1olem  8608  xlt2add  12641  hashfun  13794  hashtpg  13839  fsumcl2lem  15079  fprodcl2lem  15295  gcdeq0  15854  lcmeq0  15933  lcmfeq0b  15963  phibndlem  16096  abvn0b  20066  cfinufil  22531  isxmet2d  22932  i1fres  24307  tdeglem4  24659  ply1domn  24722  pilem2  25045  isnsqf  25718  ppieq0  25759  chpeq0  25790  chteq0  25791  ltrnatlw  37441  bcc0  40982
  Copyright terms: Public domain W3C validator