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

Theorem necon4ad 2800
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 134 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2799 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 33 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon1d  2803  fisseneq  8033  f1finf1o  8049  dfac5  8811  isf32lem9  9043  fpwwe2  9321  qextlt  11869  qextle  11870  xsubge0  11922  hashf1  13052  climuni  14079  rpnnen2lem12  14741  fzo0dvdseq  14831  4sqlem11  15445  haust1  20913  deg1lt0  23599  ply1divmo  23643  ig1peu  23679  dgrlt  23770  quotcan  23812  fta  24550  atcv0eq  28415  erdszelem9  30228  poimirlem23  32385  poimir  32395  lshpdisj  33075  lsatcv0eq  33135  exatleN  33491  atcvr0eq  33513  cdlemg31c  34788  jm2.19  36361  jm2.26lem3  36369  dgraa0p  36521
  Copyright terms: Public domain W3C validator