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

Theorem necon2ad 2955
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 2954 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2940
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 2941
This theorem is referenced by:  necon2d  2963  prneimg  4813  tz7.2  5618  nordeq  6337  xpord3inddlem  8087  omxpenlem  9020  pr2neOLD  9946  cflim2  10204  cfslb2n  10209  ltne  11257  sqrt2irr  16136  rpexp  16603  pcgcd1  16754  plttr  18236  odhash3  19363  lbspss  20558  nzrunit  20753  en2top  22351  fbfinnfr  23208  ufileu  23286  alexsubALTlem4  23417  lebnumlem1  24340  lebnumlem2  24341  lebnumlem3  24342  ivthlem2  24832  ivthlem3  24833  dvne0  25391  deg1nn0clb  25471  lgsmod  26687  nodenselem4  27051  nodenselem5  27052  nodenselem7  27054  noinfbnd2lem1  27094  slerec  27180  addsval  27296  axlowdimlem16  27948  upgrewlkle2  28596  wlkon2n0  28656  pthdivtx  28719  normgt0  30111  pmtrcnel  31989  lindsadd  36117  poimirlem16  36140  poimirlem17  36141  poimirlem19  36143  poimirlem21  36145  poimirlem27  36151  islln2a  38026  islpln2a  38057  islvol2aN  38101  dalem1  38168  trlnidatb  38686  ensucne0OLD  41890  lswn0  45722  nnsum4primeseven  46078  nnsum4primesevenALTV  46079  dignn0flhalflem1  46787
  Copyright terms: Public domain W3C validator