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

Theorem necon4bd 3036
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 3032 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 132 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  om00  8191  pw2f1olem  8610  xlt2add  12643  hashfun  13788  hashtpg  13833  fsumcl2lem  15078  fprodcl2lem  15294  gcdeq0  15855  lcmeq0  15934  lcmfeq0b  15964  phibndlem  16097  abvn0b  20005  cfinufil  22466  isxmet2d  22866  i1fres  24235  tdeglem4  24583  ply1domn  24646  pilem2  24969  isnsqf  25640  ppieq0  25681  chpeq0  25712  chteq0  25713  ltrnatlw  37201  bcc0  40552
  Copyright terms: Public domain W3C validator