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

Theorem necon4ad 2958
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 2957 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2939
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 2940
This theorem is referenced by:  necon1d  2961  fisseneq  9294  f1finf1o  9306  f1finf1oOLD  9307  dfac5  10170  isf32lem9  10402  fpwwe2  10684  qextlt  13246  qextle  13247  xsubge0  13304  hashf1  14497  climuni  15589  rpnnen2lem12  16262  fzo0dvdseq  16361  4sqlem11  16994  haust1  23361  deg1lt0  26131  ply1divmo  26176  ig1peu  26215  dgrlt  26307  quotcan  26352  fta  27124  atcv0eq  32399  erdszelem9  35205  poimirlem23  37651  poimir  37661  lshpdisj  38989  lsatcv0eq  39049  exatleN  39407  atcvr0eq  39429  cdlemg31c  40702  itrere  42358  sn-itrere  42503  sn-retire  42504  jm2.19  43010  jm2.26lem3  43018  dgraa0p  43166
  Copyright terms: Public domain W3C validator