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

Theorem necon4bd 2949
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 2945 . 2 (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3 notnotr 130 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴 = 𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wne 2929
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 206  df-ne 2930
This theorem is referenced by:  om00  8596  pw2f1olem  9101  xlt2add  13274  hashfun  14432  hashtpg  14482  fsumcl2lem  15713  fprodcl2lem  15930  gcdeq0  16495  lcmeq0  16574  lcmfeq0b  16604  phibndlem  16742  abvn0b  21269  cfinufil  23876  isxmet2d  24277  i1fres  25679  tdeglem4  26039  tdeglem4OLD  26040  ply1domn  26104  pilem2  26434  isnsqf  27112  ppieq0  27153  chpeq0  27186  chteq0  27187  ltrnatlw  39783  bcc0  43916
  Copyright terms: Public domain W3C validator