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

Theorem necon4ad 2990
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 139 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2989 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2971
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 199  df-ne 2972
This theorem is referenced by:  necon1d  2993  fisseneq  8413  f1finf1o  8429  dfac5  9237  isf32lem9  9471  fpwwe2  9753  qextlt  12283  qextle  12284  xsubge0  12340  hashf1  13490  climuni  14624  rpnnen2lem12  15290  fzo0dvdseq  15384  4sqlem11  15992  haust1  21485  deg1lt0  24192  ply1divmo  24236  ig1peu  24272  dgrlt  24363  quotcan  24405  fta  25158  atcv0eq  29763  erdszelem9  31698  poimirlem23  33921  poimir  33931  lshpdisj  35008  lsatcv0eq  35068  exatleN  35425  atcvr0eq  35447  cdlemg31c  36720  jm2.19  38345  jm2.26lem3  38353  dgraa0p  38504
  Copyright terms: Public domain W3C validator