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

Theorem necon4ad 2959
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon4ad.1 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
Assertion
Ref Expression
necon4ad (𝜑 → (𝜓𝐴 = 𝐵))

Proof of Theorem necon4ad
StepHypRef Expression
1 notnot 142 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2958 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  necon1d  2962  fisseneq  9293  f1finf1o  9305  f1finf1oOLD  9306  dfac5  10169  isf32lem9  10401  fpwwe2  10683  qextlt  13245  qextle  13246  xsubge0  13303  hashf1  14496  climuni  15588  rpnnen2lem12  16261  fzo0dvdseq  16360  4sqlem11  16993  haust1  23360  deg1lt0  26130  ply1divmo  26175  ig1peu  26214  dgrlt  26306  quotcan  26351  fta  27123  atcv0eq  32398  erdszelem9  35204  poimirlem23  37650  poimir  37660  lshpdisj  38988  lsatcv0eq  39048  exatleN  39406  atcvr0eq  39428  cdlemg31c  40701  itrere  42353  sn-itrere  42498  sn-retire  42499  jm2.19  43005  jm2.26lem3  43013  dgraa0p  43161
  Copyright terms: Public domain W3C validator