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

Theorem necon4ad 3035
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 3034 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 3017
This theorem is referenced by:  necon1d  3038  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  21890  deg1lt0  24614  ply1divmo  24658  ig1peu  24694  dgrlt  24785  quotcan  24827  fta  25585  atcv0eq  30084  erdszelem9  32344  poimirlem23  34797  poimir  34807  lshpdisj  36005  lsatcv0eq  36065  exatleN  36422  atcvr0eq  36444  cdlemg31c  37717  jm2.19  39470  jm2.26lem3  39478  dgraa0p  39629
  Copyright terms: Public domain W3C validator