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

Theorem necon2ad 3031
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon2ad.1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Assertion
Ref Expression
necon2ad (𝜑 → (𝜓𝐴𝐵))

Proof of Theorem necon2ad
StepHypRef Expression
1 notnot 144 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
32necon3bd 3030 . 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:  necon2d  3039  prneimg  4779  tz7.2  5533  nordeq  6204  omxpenlem  8607  pr2ne  9420  cflim2  9674  cfslb2n  9679  ltne  10726  sqrt2irr  15592  rpexp  16054  pcgcd1  16203  plttr  17570  odhash3  18632  lbspss  19785  nzrunit  19970  en2top  21523  fbfinnfr  22379  ufileu  22457  alexsubALTlem4  22588  lebnumlem1  23494  lebnumlem2  23495  lebnumlem3  23496  ivthlem2  23982  ivthlem3  23983  dvne0  24537  deg1nn0clb  24613  lgsmod  25827  axlowdimlem16  26671  upgrewlkle2  27316  wlkon2n0  27376  pthdivtx  27438  normgt0  28832  pmtrcnel  30661  nodenselem4  33089  nodenselem5  33090  nodenselem7  33092  slerec  33175  lindsadd  34767  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem21  34795  poimirlem27  34801  islln2a  36535  islpln2a  36566  islvol2aN  36610  dalem1  36677  trlnidatb  37195  ensucne0OLD  39776  lswn0  43451  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  dignn0flhalflem1  44573
  Copyright terms: Public domain W3C validator