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

Theorem necon2ad 2945
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 142 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
32necon3bd 2944 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1534  wne 2930
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 206  df-ne 2931
This theorem is referenced by:  necon2d  2953  prneimg  4853  tz7.2  5656  nordeq  6384  xpord3inddlem  8157  omxpenlem  9100  pr2neOLD  10038  cflim2  10294  cfslb2n  10299  ltne  11349  sqrt2irr  16243  rpexp  16716  pcgcd1  16871  plttr  18359  odhash3  19567  nzrunit  20499  lbspss  21053  en2top  22973  fbfinnfr  23830  ufileu  23908  alexsubALTlem4  24039  lebnumlem1  24972  lebnumlem2  24973  lebnumlem3  24974  ivthlem2  25466  ivthlem3  25467  dvne0  26029  deg1nn0clb  26111  lgsmod  27346  nodenselem4  27711  nodenselem5  27712  nodenselem7  27714  noinfbnd2lem1  27754  sltne  27794  slerec  27843  cuteq1  27857  addsval  27970  axlowdimlem16  28885  upgrewlkle2  29537  wlkon2n0  29597  pthdivtx  29660  normgt0  31054  pmtrcnel  32968  lindsadd  37324  poimirlem16  37347  poimirlem17  37348  poimirlem19  37350  poimirlem21  37352  poimirlem27  37358  islln2a  39226  islpln2a  39257  islvol2aN  39301  dalem1  39368  trlnidatb  39886  ensucne0OLD  43231  lswn0  47049  nnsum4primeseven  47405  nnsum4primesevenALTV  47406  dignn0flhalflem1  48036
  Copyright terms: Public domain W3C validator