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

Theorem necon2ad 3002
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 3001 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 2987
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 210  df-ne 2988
This theorem is referenced by:  necon2d  3010  prneimg  4745  tz7.2  5503  nordeq  6178  omxpenlem  8601  pr2ne  9416  cflim2  9674  cfslb2n  9679  ltne  10726  sqrt2irr  15594  rpexp  16054  pcgcd1  16203  plttr  17572  odhash3  18693  lbspss  19847  nzrunit  20033  en2top  21590  fbfinnfr  22446  ufileu  22524  alexsubALTlem4  22655  lebnumlem1  23566  lebnumlem2  23567  lebnumlem3  23568  ivthlem2  24056  ivthlem3  24057  dvne0  24614  deg1nn0clb  24691  lgsmod  25907  axlowdimlem16  26751  upgrewlkle2  27396  wlkon2n0  27456  pthdivtx  27518  normgt0  28910  pmtrcnel  30783  nodenselem4  33304  nodenselem5  33305  nodenselem7  33307  slerec  33390  lindsadd  35050  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem21  35078  poimirlem27  35084  islln2a  36813  islpln2a  36844  islvol2aN  36888  dalem1  36955  trlnidatb  37473  ensucne0OLD  40236  lswn0  43959  nnsum4primeseven  44316  nnsum4primesevenALTV  44317  dignn0flhalflem1  45027
  Copyright terms: Public domain W3C validator