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

Theorem necon2ad 2976
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 139 . 2 (𝜓 → ¬ ¬ 𝜓)
2 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
32necon3bd 2975 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1507  wne 2961
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 199  df-ne 2962
This theorem is referenced by:  necon2d  2984  prneimg  4653  tz7.2  5385  nordeq  6042  omxpenlem  8408  pr2ne  9219  cflim2  9477  cfslb2n  9482  ltne  10531  sqrt2irr  15456  rpexp  15914  pcgcd1  16063  plttr  17432  odhash3  18456  lbspss  19570  nzrunit  19755  en2top  21291  fbfinnfr  22147  ufileu  22225  alexsubALTlem4  22356  lebnumlem1  23262  lebnumlem2  23263  lebnumlem3  23264  ivthlem2  23750  ivthlem3  23751  dvne0  24305  deg1nn0clb  24381  lgsmod  25595  axlowdimlem16  26440  upgrewlkle2  27085  wlkon2n0  27144  pthdivtx  27212  normgt0  28677  nodenselem4  32712  nodenselem5  32713  nodenselem7  32715  slerec  32798  lindsadd  34326  poimirlem16  34349  poimirlem17  34350  poimirlem19  34352  poimirlem21  34354  poimirlem27  34360  islln2a  36098  islpln2a  36129  islvol2aN  36173  dalem1  36240  trlnidatb  36758  lswn0  42976  nnsum4primeseven  43333  nnsum4primesevenALTV  43334  dignn0flhalflem1  44043
  Copyright terms: Public domain W3C validator