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

Theorem necon2ad 2838
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 2837 . 2 (𝜑 → (¬ ¬ 𝜓𝐴𝐵))
41, 3syl5 34 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  necon2d  2846  prneimg  4419  tz7.2  5127  nordeq  5780  omxpenlem  8102  pr2ne  8866  cflim2  9123  cfslb2n  9128  ltne  10172  sqrt2irr  15023  rpexp  15479  pcgcd1  15628  plttr  17017  odhash3  18037  lbspss  19130  nzrunit  19315  en2top  20837  fbfinnfr  21692  ufileu  21770  alexsubALTlem4  21901  lebnumlem1  22807  lebnumlem2  22808  lebnumlem3  22809  ivthlem2  23267  ivthlem3  23268  dvne0  23819  deg1nn0clb  23895  lgsmod  25093  axlowdimlem16  25882  upgrewlkle2  26558  wlkon2n0  26618  pthdivtx  26681  normgt0  28112  nodenselem4  31962  nodenselem5  31963  nodenselem7  31965  slerec  32048  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem21  33560  poimirlem27  33566  islln2a  35121  islpln2a  35152  islvol2aN  35196  dalem1  35263  trlnidatb  35782  lswn0  41705  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator