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

Theorem necon4ad 2962
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 138 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2961 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wne 2943
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 197  df-ne 2944
This theorem is referenced by:  necon1d  2965  fisseneq  8331  f1finf1o  8347  dfac5  9155  isf32lem9  9389  fpwwe2  9671  qextlt  12239  qextle  12240  xsubge0  12296  hashf1  13443  climuni  14491  rpnnen2lem12  15160  fzo0dvdseq  15254  4sqlem11  15866  haust1  21377  deg1lt0  24071  ply1divmo  24115  ig1peu  24151  dgrlt  24242  quotcan  24284  fta  25027  atcv0eq  29578  erdszelem9  31519  poimirlem23  33765  poimir  33775  lshpdisj  34796  lsatcv0eq  34856  exatleN  35213  atcvr0eq  35235  cdlemg31c  36509  jm2.19  38086  jm2.26lem3  38094  dgraa0p  38245
  Copyright terms: Public domain W3C validator