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

Theorem necon2ad 2947
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 136 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
32necon3bd 2946 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1632  wne 2932
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 2933
This theorem is referenced by:  necon2d  2955  prneimg  4532  tz7.2  5250  nordeq  5903  omxpenlem  8226  pr2ne  9018  cflim2  9277  cfslb2n  9282  ltne  10326  sqrt2irr  15178  rpexp  15634  pcgcd1  15783  plttr  17171  odhash3  18191  lbspss  19284  nzrunit  19469  en2top  20991  fbfinnfr  21846  ufileu  21924  alexsubALTlem4  22055  lebnumlem1  22961  lebnumlem2  22962  lebnumlem3  22963  ivthlem2  23421  ivthlem3  23422  dvne0  23973  deg1nn0clb  24049  lgsmod  25247  axlowdimlem16  26036  upgrewlkle2  26712  wlkon2n0  26772  pthdivtx  26835  normgt0  28293  nodenselem4  32143  nodenselem5  32144  nodenselem7  32146  slerec  32229  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem21  33743  poimirlem27  33749  islln2a  35306  islpln2a  35337  islvol2aN  35381  dalem1  35448  trlnidatb  35967  lswn0  41890  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  dignn0flhalflem1  42919
  Copyright terms: Public domain W3C validator