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

Theorem necon4ad 3040
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 144 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 3039 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3021
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 3022
This theorem is referenced by:  necon1d  3043  fisseneq  8718  f1finf1o  8734  dfac5  9543  isf32lem9  9772  fpwwe2  10054  qextlt  12586  qextle  12587  xsubge0  12644  hashf1  13805  climuni  14899  rpnnen2lem12  15568  fzo0dvdseq  15663  4sqlem11  16281  haust1  21879  deg1lt0  24603  ply1divmo  24647  ig1peu  24683  dgrlt  24774  quotcan  24816  fta  25574  atcv0eq  30073  erdszelem9  32333  poimirlem23  34785  poimir  34795  lshpdisj  35993  lsatcv0eq  36053  exatleN  36410  atcvr0eq  36432  cdlemg31c  37705  jm2.19  39458  jm2.26lem3  39466  dgraa0p  39617
  Copyright terms: Public domain W3C validator