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

Theorem necon4ad 2842
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 136 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon4ad.1 . . 3 (𝜑 → (𝐴𝐵 → ¬ 𝜓))
32necon1bd 2841 . 2 (𝜑 → (¬ ¬ 𝜓𝐴 = 𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  necon1d  2845  fisseneq  8212  f1finf1o  8228  dfac5  8989  isf32lem9  9221  fpwwe2  9503  qextlt  12072  qextle  12073  xsubge0  12129  hashf1  13279  climuni  14327  rpnnen2lem12  14998  fzo0dvdseq  15092  4sqlem11  15706  haust1  21204  deg1lt0  23896  ply1divmo  23940  ig1peu  23976  dgrlt  24067  quotcan  24109  fta  24851  atcv0eq  29366  erdszelem9  31307  poimirlem23  33562  poimir  33572  lshpdisj  34592  lsatcv0eq  34652  exatleN  35008  atcvr0eq  35030  cdlemg31c  36304  jm2.19  37877  jm2.26lem3  37885  dgraa0p  38036
  Copyright terms: Public domain W3C validator